Fermat's Last Theorem Machine-Verified in Lean
Highlights
The biggest event this issue is the complete machine verification of Fermat's Last Theorem in Lean: Anthropic announced that Claude, in 11 days, on the Prove2Me platform, essentially autonomously wrote a complete Lean proof of FLT—about 13 million lines and 29,500 intermediate theorems, relying only on three standard axioms of Lean, with the comparator confirming the statement matches Mathlib's FLT. This is the first time a neural theorem prover has tackled a major open problem, directly continuing the AlphaProof trajectory. But the community corrects the narrative: the Imperial College FLT project led by Buzzard provided years of library groundwork and a roadmap, while Anthropic's technical appendix honestly notes the 'pending independent re-check' status. This reminds us: verification passing ≠ reusable, and a 13-million-line proof that is 5× the size of Mathlib is 'not intended for upstreaming.'
Running parallel to scale is the theme of trust infrastructure. Lean 4.32.2 fixed a soundness bug in the kernel: a phantom type parameter in nested inductive types could let a malicious metaprogram trick the kernel into accepting a proof of False, and the bug remained exploitable even under the comparator; only the independent Rust kernel nanoda was unaffected—but exploiting it required simultaneously hitting two unrelated bugs in both the Lean and nanoda kernels. This underscores the necessity of multi-kernel re-verification and gave rise to the Palomar registry, a community trust layer, with comprehensive commentary framing it within the 'proof abundance' narrative.
On the methodology front, this issue's work pushes evaluation from binary judgments to fine-grained diagnostics. ShadowBench uses shadow theorem sets with bidirectional implication checks to assess semantic alignment; ProofJudge scores proof quality along five dimensions beyond correctness; FormalRx proposes a 28-class error taxonomy with localization and repair suggestions; FaithformBench uses perturbation to quantify faithfulness and reveals 'sycophancy' in auto-formalizers. On the RL side, Process-Verified RL uses Lean's tactic-level feedback as dense rewards, Reward-Oracle MCTS treats the compiler purely as a scalar reward oracle with exhaustive axiom-level auditing, and ProofEvolve combines evolutionary archives with kernel-verified AND-OR proof DAGs for cross-goal inheritance of verified subproofs.
Community and Updates
- Fermat's Last Theorem formalized: Anthropic announcement and technical appendix document Claude's 11-day, ~13-million-line proof on Prove2Me; community perspective emphasizes the Imperial College FLT project's long-term groundwork and Claude's actual role.
- Kernel soundness bug: Lean 4.32.2 fixes a nested-inductive phantom parameter exploit; postmortem records the nanoda kernel's independence and the value of multi-kernel verification, and discloses OpenAI's role in discovering the additional kernel flaw.
- Trust infrastructure: The Palomar registry introduces Comparator-based statement/proof separation, formalization.yaml provenance tracking, and Verso-based rendering; Kim Morrison's announcement and comprehensive commentary frame it within the 'proof abundance' narrative.
- Jacobian conjecture counterexample: mathlib PR #42116 formalizes Alpöge's counterexample over ℚ³ (Jacobian determinant −2 but non-injective), with disproof independently corresponding.
- Mathlib progress: Størmer's theorem, Amice transforms, and addition chains for exponentiation bounds were merged, with the addition chain work directly serving the Scholz conjecture.
- Ecosystem roadmap: Lean FRO's Year 4 roadmap for Sep 2026–Feb 2027 prioritizes typeclass caching, fast failure for grind/bv_decide, Python FFI, and explicitly states that AI-generated proofs are becoming a primary use case.
Open Questions
- FLT proof 'verified but not reusable' (13 million lines, not intended for upstreaming): When a machine-verified artifact cannot be maintained by humans, reused, or merged into Mathlib, what does 'formalized' actually mean? How much larger does the gap between 'kernel-accepted' and 'reusable library contribution' become at FLT scale?
- Multi-kernel re-verification as default: The 4.32.2 bug required hitting two unrelated bugs in both Lean and nanoda simultaneously; does this support or undermine the case for mandatory multi-kernel checking? Can the Palomar Comparator become the community default?
- Unifying fine-grained evaluation frameworks: ShadowBench, ProofJudge, FormalRx, and FaithformBench each propose different diagnostic dimensions; can these be consolidated into a standard protocol for auto-formalization evaluation, enabling cross-system comparison and direct feedback into proof search training?
Papers in this issue
Prove2Me enables large-scale formalization by having AI agents prove audited statements on consumer subscriptions, cutting costs three orders of magnitude versus centralized swarms.
Editor's noteProve2Me is the platform hosting the FLT formalization and the biggest community event this issue. Its key increment is decentralized open collaboration: a proof-sketches mechanism decomposes open theorems into atomic subproblems, cross-agent inheritance, an immutable Formalpedia corpus for reuse, and a mission mechanism where humans audit only the core while agents freely introduce intermediate lemmas. Compared to centralized swarm approaches, it removes single-organization compute bottlenecks and merge-queue serialization—essential for understanding how 'internet-scale formalization' can work.
SA-PASS, a Lean-verified bidirectional implication metric, evaluates semantic alignment in autoformalization with 98.8% expert agreement, revealing current systems compile at 61.8% but align semantically at only 11.2%.
Editor's noteShadowBench uses a set of 'shadow theorems' with forward and backward implication checks to evaluate semantic alignment of auto-formalization, building the ShadowBench benchmark and achieving 98.8% expert agreement. Its increment: the shadow set is constructed once by experts and verified complete in Lean, enabling reusable evaluation of any generated result without over-reliance on reference phrasing; bidirectional implication simultaneously rejects weakened and strengthened statements, overcoming the defects of compile-rate and fixed-reference equivalence checks. Code and data are public—a must-read for auto-formalization evaluation.
A three-role MCTS treating the compiler as a pure reward oracle achieves 87.1% on MiniF2F with 32.8% fewer tokens, but reveals sorryAx exploits only kernel-level auditing detects.
Editor's noteThis work proposes a three-role MCTS framework that treats the Lean 4 compiler purely as a scalar reward oracle—UCB-guided tree updates do not feed error content back into the generation context, avoiding compiler-feedback contamination of the generation distribution. Its exhaustive axiom-level audit reveals proofs that depend on sorryAx yet pass standard checks, a key methodological increment for reliable evaluation. For those designing agentic proof search and verification pipelines, the kernel-level audit section is especially worth close reading.
Process-verified reinforcement learning using Lean's tactic-level feedback with first-error credit assignment improves theorem proving accuracy over outcome-only RL baselines.
Editor's noteThis work uses Lean's tactic-level feedback as dense, verifier-grounded rewards for GRPO-style RL, with first-error propagation and first-token credit assignment. Compared to DeepSeek-Prover-V1.5 (result-only rewards) and Lean-STaR (Lean only during reasoning), it is a substantive increment: it formalizes Lean's symbolic feedback into scalar training signals, achieving stable improvements on MiniF2F and ProofNet without natural-language guidance or external PRMs. The credit-assignment and reward-strategy ablations are directly valuable for designing Lean RL pipelines.
ProofEvolve achieves 57.8% average solve rate on competition benchmarks by using kernel-verified closure as graded fitness and reusing proven proof schemas across problems.
Editor's noteProofEvolve combines evolutionary computation's behavior archives (MAP-Elites) with kernel-verified AND-OR proof DAGs, proposing the verified closure ρ as a kernel-grounded fitness function and achieving cross-goal inheritance of verified subproofs via typed schema recombination. Compared to LEAP from Issue 2, LEAP's DAG memory is limited to the current goal, while ProofEvolve extracts closed sub-DAGs into a persistent schema library reused in later proofs; the 2.7× improvement in cross-problem reuse experiments provides actionable architectural insights.
ProofJudge, an agentic LLM judge with Lean tool access, aligns with human Mathlib reviewers on proof quality 80.8% of the time, far exceeding chance.
Editor's noteProofJudge is the first tool-grounded LLM-as-judge system, scoring Lean 4 formal proof quality along five dimensions beyond correctness (library utilization, automation adaptation, structural clarity, statement quality, Mathlib conventions) and constructing a dataset of 218 Mathlib PR statement pairs. It directly addresses the gap between 'kernel-valid proofs' and 'library contributions humans value'; all judges recover human reviewer preferences significantly better than random, making it an actionable evaluation tool beyond benchmark scores.
FormalRx introduces a taxonomy-driven diagnostic framework that outperforms baselines in autoformalization error categorization by 23.4 F1 points, enabling actionable, fine-grained evaluation beyond binary verdicts.
Editor's noteFormalRx advances auto-formalization evaluation from binary judgment to fine-grained diagnosis: it proposes a 28-class SCI error taxonomy (semantic/constraint/implementation three dimensions) and trains a single 8B model to simultaneously perform alignment judgment, error classification, localization, and repair in one forward pass. Compared to FaithSieve from Issue 3 and Beyond Compilation from Issue 1, it is the first to provide actionable error localization and repair suggestions rather than just judgment or classification; the unified generative architecture avoids cascading error propagation. Code, data, and weights are all public.
FaithformBench reveals that specialized autoformalisation systems silently correct invalid reasoning steps, creating a validity-sycophancy tension that undermines chain-of-thought verification.
Editor's noteFaithformBench proposes annotation-free faithfulness evaluation for auto-formalization: it automatically generates perturbed reasoning steps and evaluates faithfulness on both positive examples (validity preservation) and negative examples (invalidity preservation), and is the first to systematically reveal the 'sycophancy' phenomenon in AF systems—silently correcting invalid inputs into provable statements. Complementary to Pistis and Faithfulness Gap (which rely on human annotations or LLM judgments), its perturbation-plus-validity-preservation paradigm has direct value for designing trustworthy formalization pipelines.
Compiler-guided proof search alternating between two complementary LLMs with pairwise comparison and stagnation detection improves Lean 4 theorem proving pass rates by up to 12.66 points over single-model baselines.
Editor's noteThis work explicitly models proof search as an exploration-exploitation tradeoff: a dual-model (general + specialized) generates diverse starting points, a compiler-grounded pairwise comparison serves as the search controller deciding whether to keep/replace the current best proof, and resampling is triggered on stagnation. It is the first to systematically quantify the decisive impact of starting-point choice on refinement outcomes (inter-WP std 3.36 vs intra-WP 2.41), as well as trajectory-level insights such as roughly half of refinement proposals being rejected and 39.5% of successes coming from retained states. Complementary to training-based methods, its pure-inference structured control is lighter-weight.
