Geometric Analysis Enters Lean: The Dual Milestone of Hamilton's Theorem and Verification Boundaries
Highlights of This Issue
The main theme of this issue is "formalization crosses from algebra, number theory, and combinatorics into geometric analysis, while the verification boundary itself becomes the object under scrutiny." On the geometric analysis side, A Lean Formalization of Hamilton's Three-Manifold Theorem completes for the first time in Lean 4 the full formalization of Hamilton's 1982 theorem (three-dimensional manifolds with positive Ricci curvature are spherical space forms), with the artifact comprising approximately 1.94 million lines of Lean, including short-time existence of Ricci flow, Riemannian tensor calculus, maximum principles, and pinching estimates, and employing an alternative blow-up route rather than the original normalized flow proof. This is the first time formalization has advanced to a core theorem of geometric analysis, following FormalFlow's MIP*=RE in Issue 7, and its "consumer-driven top-down descent" methodology separates mathematical direction from proof execution, offering direct lessons for agentic formalization.
On the verification boundary side, last issue we reported that the lean4lean external checker entered the release toolchain. This issue, the Collatz artifact passing two flawed checkers provides a counterexample: an AI-assisted Collatz "refutation" simultaneously passed both the Lean kernel and the independent checker nanoda, because each contained a different implementation bug (nested inductive type handling and projection node structure name checking), and was ultimately reduced to a proof of False. This reminds us that "passing the kernel" is necessary but not sufficient—the reliability of machine verification depends on checker versions and the completeness of the verification boundary, prompting the community to propose a "Lean Kernel Arena" to stress-test checker consistency. This contrasts with the comparator/nanoda dual verification of FLT in Issue 7: independent kernels remain effective, but both sides need to stay up to date.
Open-source models and library development are equally active. Mistral released Apache-2.0 Leanstral 1.5, a 119B-parameter MoE (6B active) that saturates miniF2F and scores 587/672 on PutnamBench, at roughly one percent of the cost of comparable systems, making it the only fully open-source system in the top tier of PutnamBench. On the library side, GenLimitLib and LeanPolish push forward the boundary of "libraries and data as research tools"—the former organizes a formalization library around a single research literature, while the latter systematically exposes selection effects in search-generated supervision.
Community and Developments
- Verification boundary as a stress-test object: The AI-assisted Collatz "refutation" artifact passed both checkers simultaneously because the Lean kernel and nanoda each contained a different implementation bug. Leonardo de Moura's kernel soundness postmortem details the two defects—nested inductive types and projection nodes—and their fixes; the community has since proposed a "Lean Kernel Arena" to stress-test checker consistency. The lesson is that machine verification still depends on checker versions and the completeness of the verification boundary, and independent kernels require both sides to stay current.
- New benchmark for open-source proof models: Mistral released Leanstral 1.5, Apache-2.0 licensed, 119B-parameter MoE (6B active), saturating miniF2F (valid 244/244), scoring 587/672 on PutnamBench, 87% on FATE-H, 34% on FATE-X, at approximately $4 per problem, with test-time scaling improving smoothly and monotonically with token budget.
- Poincaré conjecture formalization progress: FrenzyMath (PKU BICMR) released an independent Poincaré conjecture Lean 4 formalization, verified by both the Lean build and the Comparator dual checker, explicitly testing the independent verification boundary; its differential geometry repository also serves as the reproducible foundation for this issue's Hamilton theorem artifact (see Highlights).
- Mathlib roadmap: The Mathlib Initiative released its October 2026 to March 2027 roadmap, listing AI integration (Formal Frontier automated formalization specifications and tools, Formal Commons federated ecosystem protocols) as near-term priorities, and explicitly adopting "scalability" rather than "line counts/theorem counts" as the evaluation criterion for automated formalization artifacts.
- Formalization gap counterexample: Reports indicate that OpenAI's unreleased model Astra produced Lean certificates for ten open problems, after which one result was refuted by a formalization gap—the existence of a certificate alone is insufficient as proof, echoing this issue's verification boundary theme from the Collatz event.
Open Questions
- The Collatz event shows that "passing the kernel" depends on checker versions and the completeness of the verification boundary—last issue's proposal of independent kernel verification as the default is now complicated by the fact that independent kernels can also be deceived by the same artifact (two different bugs). Can "checker consistency stress testing" be standardized as a mandatory reporting item for long-term formalization projects, making the Lean Kernel Arena a routine evaluation axis alongside benchmarks?
- The Hamilton theorem formalization adopts the blow-up route rather than Hamilton's original normalized flow proof—"which proof route to formalize" is essentially a trade-off between mathematical direction and formalization cost. Consumer-driven top-down descent makes this trade-off explicit, but can it be unified with FormalFlow's proof-gap protocol from Issue 7 and Trellis's monotonic refinement into a general "route selection" methodology?
- GenLimitLib organizes a library around a single literature and thereby repairs proof gaps—when formalization libraries shift from "domain foundations" to "literature alignment," should library evaluation criteria also shift from theorem coverage to "practical utility for the research process" (e.g., repairing gaps, improving results, solving open problems)? Can such utility metrics be quantified and combined with Issue 7's "interestingness" measure?
Papers in this issue
Lean formally verifies Hamilton's 1982 theorem that closed 3-manifolds with positive Ricci curvature admit constant positive sectional curvature metrics, using 1.9 million lines of code.
Editor's noteCompletes for the first time in Lean 4 the full formalization of Hamilton's 1982 theorem (three-dimensional manifolds with positive Ricci curvature are spherical space forms), with the artifact comprising approximately 1.94 million lines of Lean, including short-time existence of Ricci flow (DeTurck spectral route), Riemannian tensor calculus, scalar and tensor maximum principles, three-dimensional curvature algebra, pinching preservation and improved pinching estimates, and concluding with an alternative blow-up route rather than the original normalized flow proof; the axiom audit contains only standard axioms. Compared to FormalFlow's MIP*=RE in Issue 7, the increment lies in advancing formalization to a core theorem of geometric analysis and establishing reusable geometric analysis infrastructure; the "consumer-driven top-down descent" methodology separates mathematical direction from proof execution and is worth careful reading for anyone doing research-level agentic formalization.
GenLimitLib, a 124,000-line Lean formalization of 30 papers, boosts AI proof success from 48% to 79% and yields three new mathematical results.
Editor's noteOrganizes for the first time a formalization library around a single research literature (language generation in the limit): covering 30 papers, 405 statements, and 124,000 lines of Lean, extracting shared definitions and reusable proof components across papers, and thereby repairing proof gaps in published theorems, improving impossibility results, and solving a special case of an open problem. Compared to Lean Pool in Issue 7 (merging independent projects) and MathAtlas in Issue 2 (automated formalization benchmark), the increment lies in treating the library as a "literature-aligned research tool" rather than a domain foundation or benchmark; experiments show that library access improves kernel-verified proof success rates from 48% to 79%, with direct value for designing agentic proof search.
Verified proof datasets leak search-order shortcuts that models exploit without learning math, but complete-menu supervision and whole-proof fine-tuning reveal genuine compression gains.
Editor's noteA symbolic Lean 4 proof compression pipeline, releasing 33,402 kernel-verified local edits and 65,596 associated failed attempts, and systematically exposing selection effects in search-generated supervision (first-success ordering shortcuts, deletion triviality). Compared to proof optimization systems such as ImProver and ProofOptimizer, the increment lies in explicitly separating proposal/policy/verification and using a controlled evaluation protocol with full candidate pools, frozen baselines, and symbolic fixed points to distinguish "learning to imitate search strategies" from "improving on top of search"—a long-neglected blind spot in proof compression and learning from verification search data.
Evolutionary interface design lets a frontier model mutate agent-prover tools, yielding an MCP server that boosts theorem-proving accuracy by up to 15 points while cutting costs and time by over half.
Editor's noteProposes an evolutionary agent/prover interface (MCP server) design: frontier models incrementally propose new tools, retaining only changes that improve small-model performance, with an explicit anti-cheating protocol and cross-assistant migration (Rocq to Lean). Compared to ProofEvolve in Issue 4 (evolutionary proof search) and self-modifying Lean agents, the increment lies in shifting the optimization target from proof search or agent architecture to the interface/toolset itself, validating each mutation by accuracy, cost, and wall time; rocq-mcp-evolve and the Lean port are public, with direct value for building cost-efficient Lean proof agents.
A complete Lean 4 formalisation proves classical solvability of the Dirichlet problem for linear elliptic PDEs, with every result machine-checked and no unverified steps.
Editor's noteCompletes for the first time on Lean 4/Mathlib the full formalization of linear elliptic PDE theory: Poincaré inequality, Lax–Milgram, Rellich–Kondrachov, Fredholm alternative, spectral theorem, interior regularity, and Sobolev embedding, converging to classical solvability of the Dirichlet problem, with no sorry and only standard axioms throughout. Compared to previous De Giorgi–Nash–Moser regularity and the Coq version of Lax–Milgram, the increment lies in systematically handling the entire functional analysis pipeline for divergence-form elliptic operators and independently developing the Sobolev layer in a self-contained manner; the explicit prose-to-Lean statement correspondence and reproducible artifact (fixed commit) have direct value for extending Mathlib's analysis coverage.
External knowledge graphs help weak theorem provers but hurt strong ones, with specialization in model weights far outweighing any augmentation gains.
Editor's noteConstructs MathKG—a knowledge graph of 9,434 typed semantic edges (analogies, generalizations, cross-domain bridges) over 364 Mathlib theorems/definitions—and systematically ablates four augmentation modes across five models. Compared to retrieval augmentation in MathForm in Issue 3 and OProver in Issue 2, the increment lies in explicitly constructing a semantic layer rather than syntactic dependency retrieval, and providing controlled negative results: Lean fine-tuning dominates all augmentation modes (+33–38 percentage points), while knowledge graph context only helps small models and is actually harmful for large models; however, an oracle selecting modes per problem solves 6–58% more, suggesting the value of adaptive augmentation strategies.
