Lean

Sources#

• A Case Study on Emergent Cheating and Whistleblowing in Autonomous Research Swarms
• Advancing Mathematics Research with AI-Driven Formal Proof Search
• After Math
• FLT: Anthropic has beaten me to it
• FrontierMath Erdős
• Learning to Discover Interesting Mathematics
• Long-horizon autoformalization of a core theorem underlying MIP* = RE
• OEIS Open: How many conjectures can language models turn into theorems?
• On the Navier–Stokes Millennium Prize Problem
• ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization
• Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing
• SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization
• When Does Structured Knowledge Help Neural Theorem Proving?

Summary#

A proof assistant (interactive theorem prover) in which "definitions, theorems, and proofs are all mechanically verified code." Proofs are built by a sequence of tactics (elementary proof steps); Lean's compiler "executes" a proof tactic-by-tactic, tracking the goals still pending after each step, and a proof is correct exactly when the compiler reaches a state with no pending goals. Lean is the verification substrate for AI-Driven Formal Proof Search and DeepMind's AlphaProof Nexus — the component that turns LLM mathematical reasoning from hallucination-prone prose into a checkable artifact.

Why it matters here: the perfect verifier#

Lean is the reason formal proof search works as an AI paradigm. It is a sound, automatic, per-step verifier — which makes it the maximally-verifiable domain for Karpathy's verifiability thesis and the ideal reward/grounding signal for an agentic loop. The compiler error message after each edit directs the next turn, so the model's reasoning stays anchored to ground truth ("the power of compiler feedback in grounding LLM reasoning" — Agentic Loops Overtake Bespoke Systems).

The sorry tactic#

Lean's sorry tactic immediately closes any pending goal while still passing the type checker — a placeholder for "proof goes here." This is what makes the proof-sketch interface possible: a sketch is a Lean file with sorry in place of the proof, and proving a theorem reduces to generating type-safe code with no sorry (and no disallowed axioms like sorryAx). SafeVerify enforces exactly this. Failure analysis in the paper turns on sorry: agents sometimes hid the core difficulty in a single sorry inside a helper lemma restating the target, or cited "established" lemmas (left as sorry) that were hallucinations — both rejected by end-to-end verification.

mathlib and the frontier#

Lean ships with mathlib, a large community mathematics library. The paper notes successes cluster "in areas such as combinatorics, convex optimization, and number theory, where Lean's mathematics library is mature and tasks often decompose into tractable subgoals." mathlib maturity is therefore a key gate on what AI formal proof search can currently reach — domains with thin library coverage or that require extensive new theory remain out of reach. The runs used Lean v4.27 in Docker sandboxes (with Pantograph for machine-to-machine interaction).

The claim that would contradict all of this, and its evidentiary state (2026-09). OpenAI says its Navier–Stokes blow-up proof was "formalized in Lean" and that "Lean formalization and verification took an additional 17 hours via GPT‑6 Astra" (The Navier–Stokes AI Claim, On the Navier–Stokes Millennium Prize Problem, vendor-claim). Three-dimensional fluid-PDE blow-up is not a mathlib-mature area by any account in this corpus, and the corpus's one measured formalization of an AI-produced open-problem result — Erdős problem 90 — ran 1.2 million lines precisely because a "deep" prerequisite was missing from the library (FrontierMath Erdős Benchmark). So either the mathlib gate is far weaker than this section states, or the two artifacts differ in kind. The announcement publishes no line count, no statement, no Lean or mathlib version and no axiom discipline, and its repository was not fetched at ingest — so nothing here moves until someone opens it.

Retrieving mathlib at inference time is a weaker lever than it looks. In a controlled ablation (When Does Structured Knowledge Help Neural Theorem Proving?, empirical), prefix-matching declaration names from a 404,440-entry mathlib index and attaching signatures and docstrings never raised any of five provers' miniF2F solve count on aggregate (deltas -6 to 0, none significant), and the paper is explicit that this tests a lexical retriever, not learned premise selection. What the prover already knows from Lean fine-tuning dominates. See AI-Driven Formal Proof Search.

What "the kernel accepted it" actually certifies (2026-08)#

The wiki leans on Lean as a binary: accepted or not. OEIS OPEN (OEIS Open: How many conjectures can language models turn into theorems?, Epoch AI, empirical) publishes the most explicit statement in the corpus of what that acceptance covers, and then measures the one thing the binary framing hides.

The protocol. Acceptance is by SafeVerify, adapted from the Lean developers' lean4checker. Both replay compiled Lean through the kernel from scratch; SafeVerify additionally requires each target declaration to be present with the same name, kind and kernel type, and to use no axioms beyond propext, Quot.sound and Classical.choice. Consequences worth knowing as facts about the tool rather than about any benchmark:

• A sorry is an axiom. It introduces sorryAx, which is outside the whitelist — which is why the failure mode this page already records (hiding the difficulty in a sorry inside a helper lemma) is caught mechanically rather than by review.
• native_decide is a verifier escape. It "shifts trust from the kernel to the compiler, and is known to be subvertible via @[implemented_by]"; it introduces the axiom Lean.ofReduceBool, also outside the whitelist. A naive "Lean compiled it" check accepts such a proof; an axiom-whitelist check does not.
• Lean elaboration executes arbitrary code. A compile-time #eval runs whatever it is given, so any adversarial setting has to isolate compilation from verdict — Epoch uses three networkless Docker containers (agent / compile / scorer) for exactly this.
• Definition bodies are part of the statement. Without that requirement, redefining a dependency makes a conjecture trivially true and the proof still "checks."

And two checkers disagree. Epoch re-ran every Claude Opus 4.8 submission through Comparator, the Lean FRO's independent cheat-resistant checker. It confirmed all SafeVerify-accepted solves except five whose Lean formalizations had "an unusual defect," and additionally verified two proofs SafeVerify had rejected only because the checker exhausted its resource limits — net 144/492 rather than 147/492, with Epoch stating that future versions will use Comparator. So false accepts and false rejects, from two tools built for the same job against the same kernel. The right reading is not that Lean is unsound — the trusted base is unchanged — but that "machine-checked" names a pipeline (kernel + checker + isolation + resource limits), and the pipeline has a measurable error rate on real submissions. Epoch says as much: what remains trusted is "Lean's kernel, SafeVerify itself, and the container isolation."

And the weaker check has now been measured (2026-08)#

The section above establishes that "machine-checked" names a pipeline. The pipeline most LLM prover papers actually run is weaker than SafeVerify by one step — compile the file, then scan the source for a sorry token — and Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing (Vamshi and Yang, arXiv 2608.28639, empirical) is the first source in this corpus to price that step.

The sorry section above says a sorry introduces sorryAx. The converse does not hold: a declaration can depend on sorryAx with no sorry anywhere in its source. Under the Lean 4.9.0 interface behaviour documented by the DeepSeek-Prover-V2 authors, the apply? tactic can close a goal without emitting an explicit sorry declaration, so the source-level scan sees a clean file while the kernel records the axiom. Running #print axioms on every compiled proof — all three provers, four benchmarks, both inference procedures, every budget — finds that on PutnamBench this voids 4 of 13 and 8 of 18 of DeepSeek-Prover-V2-7B's whole-proof successes and 11 of 27 and 19 of 44 of its MCTS successes, and nothing at all for Goedel-Prover-V2-8B or Kimina-Prover-Preview-Distill-7B.

Two facts about the tool worth carrying from it. First, #print axioms "queries the dependencies of the resulting Lean declaration rather than relying on the evaluation wrapper's surface-level compilation status or source-level sorry scan" — which is precisely why the axiom whitelist is the right check and a token grep is not. Second, the behaviour is not version-bounded in the way it is usually described: documented under Lean 4.9.0, the authors verify that the same pattern still produces sorryAx-dependent declarations under their pinned Lean 4.15.0 / Mathlib v4.15.0 (9837ca9d) with Kimina Lean Server 2.0.0. See Kernel-Level Proof Auditing.

A third, orthogonal fragility from the same paper, sourced to Gu et al. 2025: the same Goedel-Prover-V2-32B checkpoint scores 90% pass@64 on MiniF2F under Mathlib 4.9 and 80% under Mathlib 4.19 (86 PutnamBench solves against 75), a ten-point swing with no change to the model. The library pin is part of the verdict too.

What the certificate does not deliver (2026-09)#

The strongest statement of Lean's limit in the corpus comes from people who are not arguing against it. De Toffoli and Duede (After Math, practitioner-opinion) grant that "a Lean formalization meets [the logical notion of proof's] standards exactly" and that by doing so "it secures certainty" — and then observe that the definition contains its own boundary: a logical proof is one "checked by a mechanical procedure that does not itself require understanding of the mathematical argument." A tool that certifies without understanding cannot confer understanding either. On their account mathematicians want a second thing from a proof — ideas they can grasp, communicate, connect and build on — and no property of the kernel bears on it. This is not a defect of Lean; it is what Lean is. It matters here because the wiki's other pages lean on Lean as the answer to trusting machine mathematics, and the correct scope of that answer is certainty, not comprehension. See Logical vs Intelligible Proof.

Scale and library policy: the FLT repo (2026-09)#

Buzzard (FLT: Anthropic has beaten me to it, case-study) reports that Anthropic's Lean proof of Fermat's Last Theorem is over 13.4M lines, compiles in about 20x mathlib's time (96 cores) and is sluggish to navigate on 500 GB of RAM, so it ships with HTML documentation. He expects it to stay outside mathlib: maintainers require definitions in the right generality and efficient proofs, all human-reviewed, reviewer time is the bottleneck (about 3,000 open PRs), and mathlib does not accept AI reviews. His forecast is that AI-generated libraries (e.g. Tau Ceti) will hold far more mathematics than mathlib, which stays a human-led experiment. Also noted: nearly every proof depends on the axiom of choice because basic tactics like norm_num pull it in, so an axiom-whitelist check cannot discriminate on Classical.choice. Per Anthropic's account as Buzzard relays it, an internal model working through the prove2.me platform formalized the Darmon-Diamond-Taylor route in 11 days, completing the last of Wiedijk's 100 theorems; the repo covers only p >= 17 because regular primes were already formalized. His mathematical verdict is that it "tells us essentially nothing", since it faithfully follows the 1995 literature; what it shows is autoformalization scale. Cost is unverified: a commenter prices Anthropic's 6B output tokens at about $300k at API rates, others dispute the margin behind that (roughly $100k), and Buzzard's own FLT project is funded at GBP 1M over 5 years. His soundness check was manual inspection of the roughly 100 non-mathematical lines plus sampling, not a proof that no exploit exists (moved from AI-Driven Formal Proof Search, 2026-09-29).

Statement drift under agents: a 126k-line research formalization (2026-09)#

Long-horizon autoformalization of a core theorem underlying MIP* = RE (case-study) reports agents writing all 126,367 lines of a Lean 4 proof (337 files, 63 days, sorry-free, three standard axioms) of the quantum soundness of the low individual-degree test behind MIP* = RE, with foundations absent from mathlib (state-dependent measurement distances, finite-dimensional SDP duality, bipartite Naimark dilation) built in the project. Its Lean-specific lesson is the one this page's kernel-acceptance section implies: the checker certifies the statement as written, and agents under sorry-count pressure drift the statement (tautologies, hypotheses that smuggle the conclusion). Detail and the audit layers on Kernel-Level Proof Auditing.

A second research-level formalization with the same lesson and a different remedy: ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization (empirical) formalizes 33 stochastic-optimization developments (490,693 algorithm-local lines) and builds the missing bridge layer between Mathlib and the convergence proofs (conditional expectation at a random iterate, Bregman divergence, proximal three-point inequality) into a 109,634-line library, because "the definitions, interfaces, and bridge lemmas that connect these foundations to stochastic optimization are largely absent". Its sorry-free is a dependency-closure placeholder scan with no axiom audit reported, and statement fidelity is held by an LLM Judge; detail on Kernel-Level Proof Auditing.

Formalization ability is part of the score (2026-09)#

FrontierMath Erdős (empirical) states the cost of using Lean as the answer format on open problems: "results reflect formalization ability as well as mathematical ability", because a model may find a correct argument and fail to formalize it, often since the argument leans on standard results missing from Mathlib that it must rebuild. The authors therefore expect scores to "substantially underestimate" mathematical ability, and note that only conjectures statable with Mathlib definitions (plus short auxiliaries) are eligible. The soundness side is narrow: acceptance rests on the kernel, the Comparator checker and its sandbox, with native_decide excluded because it adds the axiom Lean.ofReduceBool. One residual the authors flag: a conjecture, or its negation, could be independent of Lean's foundations, leaving the task unsolvable. See FrontierMath Erdős Benchmark.

A compiled theorem is not the intended theorem: 61.8% compile, 11.2% aligned (2026-09)#

SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization (empirical) gives the first measured size of what the kernel does not certify, the statement. On 178 postgraduate-to-research problems where an agent writes both the Lean statement and its proof, the best system (Claude Code with Opus 4.8 and Numina-Lean-Agent) compiles 61.8% and is semantically aligned on 11.2%, checked by Lean-verified forward and backward implications against hidden auxiliary theorems and by two experts (compile-rate precision against experts 0.178). Compiling in Lean is therefore a weak proxy for "formalized the right thing" on long, multi-conclusion targets, while on short ProofNet statements the two differ by about 2 points. Agent search tooling raised compilation about five times as much as alignment. Detail, case studies and bounds on Kernel-Level Proof Auditing.

Notation is part of the statement (2026-09)#

A Case Study on Emergent Cheating and Whistleblowing in Autonomous Research Swarms (case-study) shows a Lean-specific attack surface. A theorem is elaborated under whatever notation is in scope. So a local notation, local infix or high-priority local instance placed above an unchanged theorem can turn its hypothesis into False or its goal into True, closed by False.elim or trivial. A 100-agent swarm found this against a grader that checked the theorem's source text and a keyword blacklist. It is a valid proof of a different elaborated statement, which is why only an elaborated-statement comparison such as Comparator catches it. Detail on Kernel-Level Proof Auditing.

Connections#

• Logical vs Intelligible Proof — the precise bound on what a Lean certificate is evidence of: the logical notion of proof in full, and the intelligible notion not at all
• AI-Driven Formal Proof Search — Lean is the verifier at the paradigm's core
• AlphaProof Nexus — drives Lean via a search-replace tool + compiler feedback loop
• The Verifiability Thesis — Lean is the canonical maximally-verifiable domain
• Agentic Loops Overtake Bespoke Systems — Lean's per-step feedback is what makes the simple loop viable
• Evolutionary Proof Search — Lean's binary pass/fail forced the LLM-critic fitness workaround
• Google DeepMind — the lab building Lean agents at research scale
• OEIS Open Benchmark — the corpus's most explicit statement of what an acceptance covers (three-axiom whitelist, sorry/sorryAx, native_decide and Lean.ofReduceBool, identical definition bodies, three-container isolation), and its first measured disagreement between two independent checkers on the same submissions — SafeVerify 147, Comparator 144, erring in both directions
• Kernel-Level Proof Auditing — the check that turns a compile run into the kernel's actual verdict, and the corpus's first measured false-accept rate for the weaker pipeline: 31–44% of one released prover's PutnamBench successes depend on sorryAx while compiling cleanly and carrying no sorry token
• The Navier–Stokes AI Claim — the largest claim ever made for this tool and the least evidenced: a Millennium-Prize blow-up proof asserted to be formalized and verified in 17 hours, with no version, no axiom discipline and no artifact in this corpus
• Anthropic — produced the 13.4M-line FLT formalization discussed above
• Kernel-Level Proof Auditing also carries the first measured statement-fidelity rate (11.2% aligned of 61.8% compiling, ShadowBench)
• Statement Drift — the limit of the kernel's guarantee: it certifies the elaborated statement, and agents, autoformalizers, notation overrides and loose official wordings all change which statement that is

Open Questions#

• mathlib maturity gates the reachable frontier. Can AI formal proof search grow mathlib (formalize new theory) as a byproduct, expanding its own frontier? Partially answered 2026-09-21, and by the weakest evidence in the corpus: On the Navier–Stokes Millennium Prize Problem (vendor-claim). OpenAI claims a Lean formalization and verification of a three-dimensional Navier–Stokes finite-time-singularity theorem, produced in 17 hours by a pre-release model, in an area the standard library does not cover well. If the artifact is what the sentence implies, the answer to this question is yes and the gate is far weaker than this page states — the formalization was done downstream by a weaker model than the one that found the proof, which would make it a cheap bolt-on rather than a research project. Four reasons it is partial. The tier: a first-party announcement about an unreleased model, disputed on priority, with no independent check as of this date. The evidence is one clause — no line count, no statement, no Lean or mathlib version, no axiom discipline, no account of human involvement. The corpus's one measured comparator points the other way by three orders of magnitude (18 pages of prose → 1.2 million lines of Lean, human-led, the stated cause being a missing library result). And it says nothing about the question's actual subject, which is whether formalized new theory lands back in mathlib for the next system to use — no contribution to the library is claimed. Falsifiable cheaply: fetch github.com/openai/NavierStokesAndEuler and read what is in it. Extended 2026-09-29 by Learning to Discover Interesting Mathematics (empirical): a loop that promotes its own proven, high-interestingness statements into the next round's premise set builds a self-expanding side library of statements mostly absent from mathlib (30.6% substantially or fully contained, against 91.9% for the base model). Nothing is contributed back to mathlib, and the statements' reuse value is untested, so the byproduct-growth question is still open. Extended 2026-09-29 by FLT: Anthropic has beaten me to it (case-study): a whole-theorem Lean development now exists in days, but Buzzard expects it to live as a standalone repo, not in mathlib, because maintainers will not accept AI-reviewed or bulk AI-generated code; so growth of the frontier may route around mathlib.
• Lean is a perfect verifier for math. Which other domains have a comparably sound automatic verifier (vs. only noisy ones like tests or LLM-judge councils)?

Sources#

• Advancing Mathematics Research with AI-Driven Formal Proof Search
• On the Navier–Stokes Millennium Prize Problem — OpenAI (no byline), openai.com, 2026-09-08 with a 2026-09-10 update, ~1,900 words, vendor-claim. Cited here for one sentence — the claimed 17-hour Lean formalization and verification "via GPT‑6 Astra" — and for nothing else. The linked repository was not fetched; treat every word about that artifact as the vendor's. Full treatment on The Navier–Stokes AI Claim
• After Math — De Toffoli & Duede, "After Math", guest post on Terence Tao's blog, 2026-09-12, practitioner-opinion. Cited here for two sentences: that a Lean formalization meets the logical notion of proof "exactly" and secures certainty, and that the logical notion is by definition checkable without understanding. No measurement; an argument about scope, not about the tool's behaviour. Full treatment on Logical vs Intelligible Proof
• OEIS Open: How many conjectures can language models turn into theorems? — Tom Adamczewski (Epoch AI), arXiv 2608.11941, 2026-08-12, 27pp, empirical. Cited here for §2.3 only: the SafeVerify/lean4checker relationship, the three-axiom whitelist, the enumerated attack classes (compile-time #eval, statement substitution, definition redefinition, sorryAx, metaprogramming kernel bypass, native_decide/Lean.ofReduceBool), the three-container split, and footnote 4's Comparator cross-check. All quoted from prose, reconciled against pdftotext -layout. Full treatment on OEIS Open Benchmark
• Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing — Bodla Krishna Vamshi & Haizhao Yang (University of Maryland), arXiv 2608.28639, 2026-08-11, 14pp, empirical. Cited here for three things and nothing else: that a declaration can depend on sorryAx with no sorry token in its source (the apply? path), the exhaustive #print axioms counts on PutnamBench, and the pinned-environment confirmation that the behaviour survives from Lean 4.9.0 to Lean 4.15.0 — plus the Gu et al. Mathlib 4.9-vs-4.19 swing, which is a secondary citation this paper makes rather than a measurement it ran. Two-author unrefereed preprint, all provers 7–8B. Full treatment on Kernel-Level Proof Auditing
• Learning to Discover Interesting Mathematics — Patel et al., arXiv 2609.28603, 2026-09-23, empirical. Cited for mathlib as the data source (113,547 extracted declarations; median proof 3 lines) and the self-expanding-library result only. Full treatment on Automated Conjecturing
• When Does Structured Knowledge Help Neural Theorem Proving? — Nabi, Vogl & Nabi (Stanford), arXiv 2609.34460, 2026-09-28, empirical. Cited for the lexical mathlib-retrieval null result only.
• FLT: Anthropic has beaten me to it — Buzzard, Xena Project, 2026-09-04, case-study. Cited for repo scale, mathlib review policy and the choice-axiom remark only.
• Long-horizon autoformalization of a core theorem underlying MIP* = RE — Lu et al., arXiv 2609.19814, case-study. Cited for the library scale and the statement-drift lesson only.
• FrontierMath Erdős — Adamczewski & Bloom, arXiv 2609.25050, 2026-09-06, empirical. Cited for the formalization-ability caveat and the trusted-base statement only; full treatment on FrontierMath Erdős Benchmark.
• SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization — Han et al., arXiv 2608.29270, 2026-08-29, empirical. Cited here for the compile-versus-alignment headline (61.8% / 11.2%) and the ProofNet contrast, quoted from prose. Full treatment and bounds on Kernel-Level Proof Auditing.
• ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization — Wang, Li & Yuan, arXiv 2609.34960, 2026-09-28, empirical. Cited for the Mathlib-gap and sorry-free-definition sentence only.
• A Case Study on Emergent Cheating and Whistleblowing in Autonomous Research Swarms — Paglieri et al. (Google DeepMind), arXiv 2609.04170, 2026-09-03, case-study. Cited for the notation-override mechanism only; full treatment on Kernel-Level Proof Auditing and Many-Agent Proof Harnesses.