Lean for Non-Mathematicians: Why Machine-Checked Proofs Beat Peer Review

Imagine a meticulous math teacher: you hand over a manuscript hundreds of pages long, and they check it against formal logical rules word for word. Gloss over a single deduction, and they will fail you on the spot. That is the core role of an interactive theorem prover such as Lean.

Where conventional computers crunch numbers for humans, Lean verifies logical reasoning. Propose that “because A, therefore B,” and Lean relentlessly demands the precise logical rule supporting the step, tracing the entire chain of inference back to foundational axioms.

Lean was first launched in 2013 by Leonardo de Moura at Microsoft Research; its current mainstream version is Lean 4, maintained by the non-profit Lean FRO. Backed by leading research institutions, this open-source software is steadily emerging as the gold standard for verifying cutting-edge mathematical proofs.

A Crisis of Trust in Mathematics: Why Leading Scholars Turned to Machines

For centuries, the bedrock of mathematical trust has rested on peer review: an author writes a manuscript, and a handful of domain experts spend months—or even years—scrutinizing it. Yet modern breakthroughs routinely stretch across hundreds of pages, drawing on sprawling cross-disciplinary machinery. Even top specialists find it hard to guarantee a review free of oversights.

Over the past three decades, several watershed moments have laid bare the limits of human auditing:

• Wiles’s Gap in Fermat’s Last Theorem: In June 1993, Andrew Wiles stunned the mathematical world by presenting a proof of Fermat’s Last Theorem. But during two months of intensive refereeing, reviewers uncovered a critical gap. Wiles and Richard Taylor then spent a full year on repairs, and the corrected version appeared in May 1995. Even a handwritten manuscript by a mathematician of Wiles’s caliber is prone to oversights—and auditing and mending them consumed enormous human effort and time.
• Voevodsky Discovering His Own Error: Fields Medalist Vladimir Voevodsky discovered in 1999 that a major paper he published seven years earlier contained a fatal flaw. That experience propelled him toward formal mathematics and Univalent Foundations, in search of a sturdier logical foundation for computer-assisted proof. As he noted in a Quanta Magazine interview: “The world of mathematics is becoming very large, the complexity is very high, and there is a danger of accumulation of mistakes.”
• The Kepler Conjecture and “99% Certainty”: In 1998, Thomas Hales announced a proof of the centuries-old Kepler conjecture on sphere packing. His submission spanned 250 pages of notes alongside 3 GB of custom code. After four years of review, a panel of 12 referees concluded they were only “99% certain” of its correctness. The remaining 1% of doubt was not dispelled until Hales’s team completed the Flyspeck project, fully formalizing the proof in software.

When proofs outgrow the limits of human cognition, the need for the guarantee—“I may not understand every detail, but I can be certain it is correct”—has steered mathematicians toward formal verification.

The Counterfeit Detector Model: Why Computer-Checked Proofs Deserve Trust

A natural first reaction is skepticism: doesn’t software have bugs? Why should we trust a computer’s verdict? Lean’s answer is not to ask for blind faith in complex software, but rather to minimize the trusted computing base to the absolute bare minimum and lay it open for scrutiny.

The Bank Teller and the Counterfeit Detector

Consider a busy bank branch processing tens of thousands of bills daily. A manager cannot guarantee every teller is honest and careful. But if every single banknote entering or leaving the vault must pass through the same open, transparent counterfeit detector governed by only a handful of rules, counterfeit bills simply cannot slip through.

In Lean’s architecture:

• The Tellers: The mathematicians, automated algorithms, or large language models (AI) that write proofs. They can be extremely complex, and they can make mistakes.
• The Counterfeit Detector: The Lean Kernel. It operates on only a handful of foundational logical rules, methodically validating every granular step of inference.

This design adheres to the de Bruijn criterion, formulated by the Dutch logician: the validity of a proof must be verifiable by a standalone kernel small enough that a person can carefully review its source code.

 Untrusted layer
 Writers, tactics,
 AI and tools
       |
       | proof terms
       v
 Lean kernel
 (trust root)
       |
       v
 Valid / invalid proof

Rejecting “Trivially Obvious” and Enabling Zero-Trust Collaboration

In traditional peer review, the easiest places for errors to hide are the leaps a paper waves through as “clearly true,” “obviously,” or “the same reasoning applies.” Lean permits no such leaps; every deduction must be spelled out according to explicit rules.

Because trust is anchored in the kernel rather than in people, any proof that passes kernel inspection is mathematically correct—no prior acquaintance or reputational endorsement required. This rigor has given rise to entirely new models of research collaboration:

• The Liquid Tensor Experiment (LTE): When Fields Medalist Peter Scholze challenged the community to verify Theorem 9.4, a team led by Johan Commelin completed the formalization in 18 months. Scholze stated plainly that Theorem 9.4 was the only core result he had ever worried about. Once it passed formal verification, he had “no doubts whatsoever” about the main proof—and called it “insane” that a proof assistant could certify cutting-edge research on such a timeline.
• Terence Tao and the PFR Project: In November 2023, after proving the Polynomial Freiman-Ruzsa (PFR) conjecture, Terence Tao launched a formalization project that community volunteers worldwide completed within weeks. Tao observed that formalization “enables large-scale mathematical collaborations without requiring collaborators to establish prior trust.” Maintainers repeatedly approved contributions from people they had never met, because the code was machine-verified as correct and visibly advanced the project.
• The community mathematical library Mathlib: More than 770 contributors worldwide have amassed over 130,000 definitions and 280,000 theorems in Mathlib, making it the shared foundation of modern formal mathematics.

What Does the Code Look Like? Three Minimal Examples, from Simple to Sophisticated

In Lean, writing a proof feels remarkably like writing code. The following examples are drawn from the official community textbook, Mathematics in Lean:

Example 1: Proving $2 + 2 = 4$

theorem easy : 2 + 2 = 4 :=
  rfl

• theorem easy: Declares a theorem named easy.
• : 2 + 2 = 4: States the mathematical proposition to be proven.
• :=: Introduces the proof term.
• rfl (reflexivity): Asserts that “both sides are fundamentally identical by definition.” Lean unfolds both expressions to their primitive definitions and accepts the proof once it confirms structural equality. If you replace 4 with 5, the compiler immediately flags an error.

Example 2: Stating Fermat’s Last Theorem with an Unfinished Proof

def FermatLastTheorem :=
  ∀ x y z n : ℕ, n > 2 ∧ x * y * z ≠ 0 → x ^ n + y ^ n ≠ z ^ n

theorem hard : FermatLastTheorem :=
  sorry

This snippet illustrates two defining aspects of Lean:

• ∀ and ℕ precisely capture the statement: “For all exponents greater than 2 and all non-zero natural numbers, the equation has no solutions.”
• sorry acts as an explicit logical IOU. Lean allows you to defer a proof step during development, but it tags the theorem as incomplete and will never let an unfinished proof pass as verified.

Example 3: Proving That Any Multiple of an Even Number Is Even

Consider proving an elementary arithmetic statement: “For any natural numbers $m$ and $n$, if $n$ is even, then $m \times n$ is also even”:

example : ∀ m n : Nat, Even n → Even (m * n) := by
  rintro m n ⟨k, hk⟩
  use m * k
  rw [hk]
  ring

• by: Switches into tactic mode, allowing you to construct the proof interactively step-by-step, much like working on a chalkboard.
• rintro, use, rw: Introduce variables, shape the goal, and substitute known hypotheses.
• ring: Invokes an automated tactic designed to handle polynomial and ring arithmetic.

The crucial insight: automated tactics like ring merely search for a derivation path. Every detailed step they generate must ultimately pass through the minimal kernel for inspection. Tactics themselves have no authority to approve a proof on their own.

Machines Are Not Omnipotent: Three Blind Spots Lean Cannot Cover

While Lean delivers extraordinarily high logical reliability, its official manual states plainly that it is no panacea—at least three blind spots remain at its edges:

Blind Spot 1: Specification Errors (Semantic Gaps)

Lean only verifies whether a proof satisfies the statement as written in code; it cannot know whether that code matches the mathematics in the author’s head.

In Google DeepMind’s open-source project, the formal Lean statement for Erdős Problem 480 was meant to require $n \ne 0$ but was mistakenly typed as $m \ne 0$. With $n = 0$, the division in the formula runs into a deliberate Lean convenience: any number divided by zero is defined to be zero. The AI quickly found a trivial proof, collapsing the inequality into "$0 \le 0$"—a mathematically vacuous tautology—and sailed through.

Similarly, a study on miniF2F—a standard benchmark for AI olympiad mathematics—revealed that over half of its Lean problem statements diverged from the original problems, with missing constraints and misplaced parentheses among the gaps.

 Intended math idea
         |
         | human translation
         v
 Lean formal statement
         |
         | kernel check
         v
 Proof validates
 the written statement
         |
         v
 Not necessarily
 the intended idea

Blind Spot 2: Axiom Contamination and Hidden Dependencies

All mathematics rests on fundamental axioms. If a proof silently introduces conflicting custom axioms, or cites a prerequisite theorem containing a sorry, the kernel will still approve the local deduction—leaving the broader result resting on unstable foundations. Lean’s remedy is not to ban axioms, but to provide transparent commands—#print axioms, for one—that let anyone audit, in a single stroke, every axiom and unfinished premise a theorem rests on, keeping its boundaries fully open.

Blind Spot 3: Potential Bugs Within the Kernel

To guard against the risk of bugs in any single verification engine, the community has built a multi-layered, independent verification ecosystem:

• lean4checker: Re-runs the compiled project through a clean kernel for a complete re-check.
• nanoda: A third-party type checker implemented from scratch in Rust by an independent community.

When multiple checkers implemented by different teams in different programming languages all validate the same proof artifact, the probability of an undetected shared vulnerability shrinks to near zero.

The Price of Prosperity: Dissenting Views and the Practical Bottlenecks of Formalization

As AI-assisted theorem proving accelerates—from Google DeepMind’s AlphaProof and AlphaGeometry 2 jointly achieving silver-medal performance at the 2024 International Mathematical Olympiad (IMO), to Anthropic’s September 2026 announcement that Claude formalized Fermat’s Last Theorem in 11 days across more than 13 million lines of code—the mathematical community has engaged in deep soul-searching:

1. Verification Is Not Discovery

Kevin Buzzard, a professor at Imperial College London who led the human formalization of Fermat’s Last Theorem, remarked after personally compiling and verifying Claude’s proof: “This formalization just follows the early literature faithfully—it adds nothing.” As mathematics, it offers no new insight; what it showcases is a breakthrough in automated formalization engineering.

2. An Unreadable Monolith of Code

The AI-generated proof spans 13.4 million lines and takes nearly 20 times longer to compile on a 96-core (CPU) workstation than the entire Mathlib library. Buzzard conceded that this codebase cannot fulfill his original vision of creating an interactive, exploratory document for human mathematicians. The machine has verified “correct”; humans have not necessarily gained “understanding.”

3. Community Review Bottlenecks and Compute Costs

The deluge of AI-generated code has also strained the open-source ecosystem. Buzzard revealed that Mathlib reviewers are extremely reluctant to review AI-generated code of uneven quality. The community currently faces a backlog of over 3,000 open pull requests (PRs), with more than 600 actively queueing for review—expert human attention remains the true bottleneck.

Moreover, formalization carries substantial resource costs. Claude’s 11-day parallel exploration completed the FLT proof, consuming roughly 6 billion output tokens (estimated at around $300,000 at market rates). By comparison, the five-year human community project led by Buzzard received roughly £1 million in grant funding from the UK’s EPSRC. Formalization tools have solved the problem of “trust,” but not yet the challenges of “understanding” and “cost.”

4. The Ultimate Goal of Mathematics Is Understanding

Mathematician Michael Harris has written against the myths surrounding the formalization craze, stressing that mathematics derives its value from the grasp of the human mind:

“We play the game to understand, not to win.” — Michael Harris

Machine-generated code that no human can read, however logically unassailable, has limited power to inspire.

 Machine proof
       |
       v
 Correctness
 (high trust)

 Human thought
       |
       v
 Intuition and insight
 (deep understanding)

Getting Started: From In-Browser Verification to Puzzle Games

For readers eager to experience interactive theorem proving firsthand, the community offers several welcoming entry points:

• Lean 4 Web Editor: No installation required—open your browser, paste any example from this article, and watch it verify in real time.
• The Natural Number Game: Originally created by Kevin Buzzard and Mohammad Pedramfar, this interactive game guides players from the definitions of $0$ and addition onward to derive arithmetic properties step by step, like puzzle levels. It is widely regarded as the best entry point for complete beginners.
• Advanced Resources: Once comfortable with the basics, dive into the community textbook Mathematics in Lean or the official guide Theorem Proving in Lean 4.

In the end, Lean is a counterfeit detector: it guarantees that every single bill is authentic, but the vision of where those inferences lead remains the domain of human intuition and insight. By handing over the tedious burden of auditing to machines, mathematicians may finally be free to focus on the true essence of their craft: understanding.