Poincaré Conjecture Completed in Lean Formalization, Verified Kernel Ships with Official Release
Highlights of This Issue
The main theme of this issue is turning "trust" from a slogan into testable infrastructure. The skepticism raised in the previous issue about "Lean verification means proof correctness" has received a direct response: the Lean team has released the first verified kernel with a consistency proof. Lean Now Ships with Verified Kernels announces con-leche (a checker written in Lean with a consistency proof) and con-ron (its Rust refinement, proven equivalent to con-leche via Aeneas), as well as lake check --paranoid multi-kernel sandbox rechecking—directly addressing the "two checkers sharing the same bug" issue exposed by the Collatz incident in the previous issue, turning kernel-level auditing from a research tool into an everyday command.
In terms of formalization scale, the landmark event of this issue is An AI-Assisted Formalization of the Poincaré Conjecture: following the Morgan–Tian route, it completes the full Lean 4 formalization of Perelman's proof, about 2.8 million lines, double-checked by Comparator and the independent Nanoda kernel. Compared to the Hamilton three-manifold theorem (key lemma) in Issue 8, it goes end-to-end through the entire conjecture and uses "mathematician-reviewed milestone statements" as a fixed interface for parallel agent work—statement review precedes proof construction. Meanwhile, How to Formalize All of Mathematics, a position paper co-signed by core Lean/Mathlib maintainers, sets community standards and a roadmap for AI-scale formalization, naming target projects such as Tau Ceti, Formal Frontier, Palomar, and Annals Challenge.
The evaluation landscape is also shifting from "isolated theorem proving" to "infrastructure building." AutoformBench (Meta, 341 tasks) embeds each task in a larger mathematical development, requiring agents to construct missing definitions and lemmas; A dataset of formalised theorem statements from the Annals of Mathematics provides 50 research-level theorem statements as a high-confidence benchmark; Aligning Faithfulness for Theory-Scale Autoformalization advances faithfulness evaluation to phrase-level alignment. Together, these three point to a judgment: statement-level formalization is rapidly saturating, and the bottleneck is shifting toward definition compatibility, infrastructure building, and semantic faithfulness.
Community and Updates
- Lean official release of verified kernel: Lean Now Ships with Verified Kernels announces con-leche (a verified kernel written in Lean, with a consistency proof via a set-theoretic model) and con-ron (a Rust refinement), as well as
lake check --paranoidwhich rechecks the entire development with four built-in kernel sandboxes. This directly responds to the aftermath of the kernel soundness bug in the previous issue, turning "multi-kernel rechecking" into an everyday command. - Community roadmap position paper: How to Formalize All of Mathematics is co-signed by Avigad, Buzzard, Commelin, Degenne, Morrison, Nash, and Topaz, setting standards for AI-scale formalization and naming targets such as Tau Ceti, Formal Frontier, Palomar, and Annals Challenge.
- Hales proposes cross-checking with about 25 independent kernels: According to community reports, in a guest post on Tao's blog, Hales suggested cross-checking proofs with about 25 independently implemented Lean kernels, and pointed out that the Collatz case shows "more does not mean independent"—two checkers may share the same bug.
- AnnalsChallenge goes live on LeanEval: The 50 research-level statements from A dataset of formalised theorem statements from the Annals of Mathematics are now on the LeanEval leaderboard, and within weeks of release, 40/50 have received community proof submissions.
- Meta releases AutoformBench: The 341 tasks in AutoformBench shift evaluation from isolated theorem proving to infrastructure building, finding that success depends more on the model's ability to construct missing formal infrastructure than on the mathematical domain.
Open Questions
- The Poincaré formalization uses "reviewed milestone statements" as a fixed interface for parallel agents, but who guarantees the faithfulness of the milestone statements themselves? Can the phrase-level alignment method from FaithAlign in this issue be used to systematically audit these interface statements, rather than relying on manual item-by-item review?
- The consistency proof of con-leche assumes the consistency of set theory (a limitation of Gödel's second incompleteness theorem), while Hales's multi-kernel cross-checking has been shown in the Collatz case to be unable to catch shared bugs—where are the trust boundaries of the "verified kernel" and "multi-kernel cross-checking" approaches respectively?
- AutoformBench finds that "constructing missing infrastructure" is the bottleneck, but its single-shot design excludes interactive repair—is this bottleneck due to model capability gaps, or because the evaluation protocol excludes the iterative loop present in real formalization?
- With 40/50 proofs submitted within weeks of the AnnalsChallenge release, does this mean "statement-level formalization" is saturating and the frontier is shifting toward definition compatibility and infrastructure building? Should Definition Grounding's ReuseBench become the standard evaluation surface for the next stage?
Papers in this issue
The Poincaré conjecture was fully formalized in Lean 4 in two weeks for $25,000 using AI agents guided by 90 mathematician-reviewed milestones as stable interfaces.
Editor's noteThe first complete AI-assisted Lean 4 formalization of the Poincaré conjecture, following the Morgan–Tian route to complete both the topological and smooth versions of Perelman's proof, about 2.8 million lines of Lean, double-checked by Comparator and the independent Nanoda kernel. Compared to the Hamilton three-manifold theorem in Issue 8 (which formalized a key lemma), the increment is completing the entire conjecture end-to-end and using "mathematician-reviewed milestone statements" as a fixed interface for parallel agent work—statement review precedes proof construction, serving as an organizational template for research-level agentic formalization. The public repository and cost record of about $25,000 make it a reproducible artifact.
ANNALSCHALLENGE, a dataset of 50 formalised Annals of Mathematics theorems in Lean 4, shows 80% were autoformalised within weeks, revealing Mathlib's growing readiness for research mathematics.
Editor's noteThe first dataset of Lean 4 theorem statements targeting contemporary pure mathematics research level (Annals of Mathematics 2020–2026): main theorems from 50 papers, double-audited by humans and AI, with original authors consulted to confirm intent, and an appendix documenting corrections of 10 missing/implicit assumptions in the papers. Compared to MathAtlas in Issue 2 (textbook-level, dependency graph evaluation), the increment lies in sourcing from top journals, emphasizing faithfulness and correctness, and being live on LeanEval to support community submissions—within weeks of release, 40/50 have proof submissions, making it a high-confidence benchmark for evaluating autoformalization and proof search.
The align-then-label framework and FaithAlign benchmark reveal state-of-the-art models miss most autoformalization defects, overlook contextual links, and rarely recognize undecidable cases.
Editor's noteThe first theory-scale faithfulness benchmark: 460 items, 4,982 phrase-level alignment links, operationalizing faithfulness evaluation as a context-aware align-then-label problem, and introducing FaithAlign-Gap (146 items) to test whether models can recognize that "missing context makes faithfulness undecidable." Compared to FormalRx in Issue 4 (28 error types) and ShadowBench (bidirectional implication), the increment is advancing from statement-level judgment to phrase-level alignment with context dependence and undecidable labels. The strongest model achieves only 4.5% full detection on multi-defect items and fails to recognize 71.8% of undecidable cases, providing a sobering baseline for evaluator design.
Learned neural evaluators predict Lean 4 proof verdicts with 87.8% accuracy at 4.2x throughput, cutting GRPO training time by 31% without performance loss.
Editor's noteTransforms Lean 4 proof candidate evaluation from "running the kernel" to a learned cascade on GPU: a single-token validity classifier plus a feedback model predicting target states and errors, trained on a 4.84M program dataset, with the two-stage evaluator achieving 87.8% accuracy in predicting acceptance of candidate proofs. The increment lies in using the predicted compiler feedback system as training signal and running Lean and the learned evaluator concurrently in GRPO, reducing training step time by about 31% while maintaining miniF2F performance—directly alleviating the verification bottleneck in RL training, with the 68,932 program benchmark and dataset publicly available.
LLM-generated Lean 4 definitions from raw textbook text fail downstream reusability 50-75% of the time, but cleaning informal text and LLM-judge screening with basic properties raises compatibility to 77.5% at 11% of formalization cost.
Editor's noteProposes "definition grounding" as a continuous judge-and-revise process to ensure formalized definitions are reusable downstream, and builds ReuseBench (8 theories, hierarchical statements D/S1–S5) to measure definition compatibility. Compared to MathAtlas in Issue 2 (isolated scoring of definitions), the increment is explicit focus on downstream compatibility: definitions formalized by agents from textbook text are only 25–50% compatible with subsequent statements, and clarifying informal definitions can improve this to 77.5%; moreover, stating only a few basic properties (without proving them) can significantly improve LLM judges' compatibility prediction at about 11% of the definition cost—a directly actionable method for building reusable formalization libraries.
IneqAgent combines LLM reasoning with symbolic computation via lemma-level MCTS to achieve 94.09% success on formal inequality proving in Lean 4, surpassing all baselines.
Editor's noteAn agentic inequality prover combining lemma-level MCTS with three complementary symbolic computation backends (SOS, Bernstein, differential substitution), first extending Kaltofen's numerical-symbolic recovery process to SOS certificates with constraints (sequential recovery), and translating certificates from the three backends into local Lean proofs. Compared to LIPS in Issue 5 and NSPI in Issue 4, the increment lies in using MCTS to uniformly coordinate lemma construction, goal reformulation, and backend selection, and systematically handling certificate recovery with equality/inequality constraints; obtaining Lean-verified strengthened results for Dittert's conjecture in dimensions four and five and an exact SOS certificate for Holens–Djokovic (4,4), with code and the LitIneq benchmark publicly available.
LEANGRAPHSEARCH uses personalized PageRank over Mathlib's formal dependency graph to boost premise retrieval recall by 12 points and improve Lean 4 proof completion by up to 40%.
Editor's noteA graph retrieval method based on Mathlib's formal dependency graph: using query-personalized PageRank to propagate over declaration dependencies, revealing supporting lemmas that are lexically dissimilar to the target but repeatedly appear in proofs of related problems, then re-ranking in two stages with semantic and graph scores. Compared to retrieval frameworks like OProver in Issue 2, the increment lies in explicitly exploiting multi-hop dependency traversal between declarations rather than only semantic similarity, integrating with agentic proof loops and analyzing cost-effectiveness, with code and benchmarks publicly available.
This paper delivers the first end-to-end machine-verified security proof of qubit BB84 QKD against coherent attacks, formalized in Lean 4 with a tighter entropy bound.
Editor's noteThe first end-to-end machine-verified composable finite-key security proof of entanglement-based qubit BB84 against coherent attacks, completed in Lean 4 using a novel LOCC-enforced protocol language, with improved conditional entropy variance bounds and reduced finite-size penalties. The increment lies in fully formalizing a complex quantum cryptographic protocol and demonstrating the use of an LLM autoformalization pipeline as a discovery machine; the open-source library provides reusable artifacts with direct value for autoformalization and formal verification researchers.
