After Fermat's Last Theorem: Readability, Soundness, and Verification Blind Spots
Highlights of This Issue
The aftermath of the formalization of Fermat's Last Theorem (FLT) became the main thread in the community this issue. Kevin Buzzard's first-hand account independently compiled and verified Anthropic's 13-million-line Lean proof using a comparator, but redefined the bottleneck from "proof generation" to "human reading and verification"—Mathlib will not accept unreadable AI-generated proofs. This directly responds to the "kernel acceptance vs. reusable library contribution" gap raised last issue: when proof size exceeds human maintainability, the value of formalization depends on readability, not just kernel acceptance.
Trust infrastructure continues to be tested. Trail of Bits report disclosed a new soundness flaw: the logical definition of String.Pos.Raw.extract behaves inconsistently with the compiled native code on extremely large position slices, enough to create a contradiction and thus "prove" Fermat's Last Theorem. Unlike the nested induction flaw in 4.32.2 from last issue, this is a model/runtime divergence rather than a kernel logic flaw, but it similarly adds the compiler to the trusted computing base, again confirming the necessity of lean4lean-style cross-verification.
On the evaluation front, multiple works this issue target the "solver decision blind spots." ProofNet-Verified audit shows that more than half of the statements in ProofNet are misformalized, directly impacting the validity of previous evaluations based on this benchmark. Meanwhile, domain-specific benchmarks (stochastic processes, quantum mechanics) and general-purpose code agents (Leanstral) are emerging, marking a shift of benchmarks from competition problems to textbook- and research-level mathematics at scale.
Community and Updates
- FLT aftermath: Buzzard's Xena blog independently verified Anthropic's FLT formalization and redefined the bottleneck as human reading/verification rather than generation; Djalil Chafai's practical report documents a case of using ChatGPT Codex CLI to generate approximately 16,400 lines of Lean formalization without sorry/axiom and plans to contribute to Mathlib.
- Soundness flaw: Trail of Bits disclosed that
String.Pos.Raw.extractmodel/runtime divergence can create contradictions, affecting up to 4.33.1, with a patch entering 4.34.0-rc1; the Lean team fixed the memory safety issue in about 90 minutes and the semantic divergence in 5 days. - Benchmark audit: ProofNet-Verified audited and corrected ProofNet/ProofNet#, finding that 55.6% of statements in ProofNet and 26.4% in ProofNet# are misformalized, and provided corrected formal proofs for all 367 statements.
- General-purpose code agent: Leanstral (119B/6B sparse MoE) saturates miniF2F within the Mistral Vibe code agent framework, solves 587/672 PutnamBench problems, and introduces the FLTEval benchmark based on PRs to the FLT repository.
- Conference updates: AITP'26 announced its agenda, including Poiroux's automated formalization of sphere packing and Frieder's AIMO update.
Open Questions
- The "kernel acceptance vs. reusable library contribution" raised last issue has a clear answer from Buzzard this issue: Mathlib will not accept unreadable AI-generated proofs. Can "readability" be quantified and used as an optimization target for proof search, rather than a post-hoc human review threshold?
- The multi-kernel cross-checking raised last issue gains new evidence this issue: Trail of Bits'
String.Pos.Raw.extractflaw adds the compiler to the trusted computing base, and it differs in nature from the nested induction flaw in 4.32.2. Can lean4lean-style cross-verification cover such "model/runtime divergence" flaws, or is a new verification layer needed? - The 55.6% misformalization rate in ProofNet implies that previous evaluation conclusions based on this benchmark need re-examination—can the "unified diagnostic protocol" proposed last issue be extended to audit the benchmark itself, allowing benchmark flaws and system flaws to be evaluated separately?
Papers in this issue
MAGENTA achieves 100% verified accuracy on AIME and HMMT benchmarks by pairing LLM reasoning with Lean 4 verification and diagnostic-guided self-correction, eliminating paraphrasing robustness gaps entirely.
Editor's noteMagenta explicitly models verification failure as an attribution problem: an error judge distinguishes mathematical errors from syntax errors, routing failures to re-derivation or local proof repair rather than simple retries; a statement judge explicitly prevents "fake certificates"—formalized statements that are unfaithful to the original problem yet pass Lean verification. Compared to Reward-Oracle MCTS from Issue 4 (treating the compiler as a pure scalar reward) and Process-Verified RL (training-based), Magenta is a training-free inference-time closed loop, and ablations show that the statement judge provides substantial gains in error certificate rate and feedback-guided correction on hard problems. Code and data are public, making it a significant increment in agentic proof search.
Generative verification, which distills an offline Z3-equivalence oracle into a reference-free, continuous score, detects verdict-preserving-unfaithful formalizations with 0.961 AUROC, beating structural and solver-only methods.
Editor's noteThis work formalizes the "verification-preserving unfaithfulness" (VPU) failure mode—incorrect encodings can successfully execute and match solver decisions yet not be equivalent to the reference—and proves that purely decision-based heuristics are mathematically limited to random levels. Its increment lies in distilling an offline Z3 equivalence oracle into a reference-free, continuous generative verifier (GenV) that can detect unfaithful formalizations even when references are absent, and mechanism analysis shows that error localization emerges without explicit training. Compared to ShadowBench (bidirectional implication of shadow theorems) and Beyond Compilation from Issue 4, GenV directly attacks the solver's "decision blind spots," providing direct value for building trustworthy automated formalization pipelines.
AxQM introduces the largest physics proof-synthesis benchmark, with 1,019 Lean-verified tasks from Nielsen and Chuang, exposing kernel-evading formalization errors.
Editor's noteAxQM is the largest physics formalization proof synthesis benchmark to date: 1019 tasks, 479 entries, all from the Nielsen-Chuang textbook, 4.1 times the size of the previous largest physics benchmark. Its core increment lies in being a census of a single book rather than sparse sampling across sources, with tasks embedded in a custom finite-dimensional quantum mechanics Lean library, and all tasks guaranteed solvable (solution library kept secret to prevent leakage); it also explicitly audits and fixes semantic flaws in predecessors like Lean-QIT-Bench, such as quantifier order errors and unconstructed circuits. In the Mathlib fork, the generalization of MultilinearMap to multilinear maps has been submitted as an upstream PR, contributing practically to the Lean ecosystem.
Nonexistence of a Strongly Regular Graph with Parameters (266,45,0,9): A Certificate-Free Lean Proof
A fully formal Lean 4 proof shows no strongly regular graph with parameters (266, 45, 0, 9) exists, using lattice and design arguments without external certificates.
Editor's noteThis work provides a certificate-free Lean 4 proof of the nonexistence of the strongly regular graph parameters (266,45,0,9), using a marked rank-24 even unimodular lattice and harmonic theta identities to replace external infeasibility certificates and classification theorems, relying only on Lean's three standard axioms and independently verified by nanoda. Compared to previous formalized nonexistence proofs relying on external certificates, its methodological increment lies in being fully self-contained and reproducible (release v2.0.0), making it an ideal artifact for testing proof search systems and trust infrastructure.
The Henstock-Kurzweil gauge integral constructs non-Gaussian functional integrals directly in real time, avoiding Wick rotation and yielding finite, smooth, machine-verified results despite divergent perturbative series.
Editor's noteThis work uses the Henstock-Kurzweil gauge integral machine to construct non-Gaussian functional integrals in a machine-checked way, avoiding Wick rotation, Wiener measure, and ζ-regularization, proving that single-mode non-Gaussian integrals are finite, strictly positive, monotone, and infinitely differentiable in the coupling λ—with derivatives given by convergent integrals rather than divergent perturbation series. Compared to previous Gaussian HK path integrals, its increment lies in advancing the construction to quartic (non-Gaussian) couplings and proving influence functional decomposition and Chernoff splitting, all without sorry and using only three standard axioms, making it a verifiable target for formalized mathematical physics.
STOCHBENCH, a 450-problem Lean 4 benchmark, shows proof agents solve only 34.9% of graduate stochastic processes problems, with rates varying 14-fold by topic.
Editor's noteStochBench is the first domain-specific Lean 4 benchmark for graduate-level stochastic processes: 450 problems covering eight topics including Markov chains, martingales, and Brownian motion, each with natural language sources and direct/abstract statement splits. Its increment lies in focusing on a single applied mathematics domain, sharing definitions, and explicitly labeling the abstraction level of statements, supporting scope-aware proof agent evaluation, filling the gap in Mathlib's coverage of stochastic processes. The baseline is a single-agent single-budget run without ablations, so 34.9% should be treated as a rough reference rather than rigorous results.
