FrenzyMath reports about 3.2 million lines of Lean and less than USD 30,000 in LLM and compute costs for the project. The repository separates the Mathlib-only endpoint statements from the proof library and preserves Comparator configuration, verifier revisions, logs and source-provenance records.
On 28 September 2026, FrenzyMath announced a complete Lean 4 formalization of the smooth and topological three-dimensional Poincaré conjecture, primarily following Morgan and Tian's exposition of the Hamilton–Perelman proof. The team reports a full Lean build and Comparator verification of two public endpoint statements using Lean's kernel and Nanoda with only the standard axioms propext, Classical.choice and Quot.sound. FrenzyMath reports that three AI developers with mathematical backgrounds and several volunteer mathematicians completed most of the work within half a month using publicly available commercial LLMs.
FrenzyMath reports about 3.2 million lines of Lean and less than USD 30,000 in LLM and compute costs for the project. The repository separates the Mathlib-only endpoint statements from the proof library and preserves Comparator configuration, verifier revisions, logs and source-provenance records. The announcement also notes that an independent team led by Ziyang Qin, Yuan Liao, Ayush Khaitan and Bennett Chow released another complete Poincaré Lean development earlier the same day; that separate arXiv paper records a full public build and says automated assistance was used for proofs and prose.
Poincaré is a foundational modern theorem whose standard proof uses a large stack of geometric analysis, topology, partial differential equations and Ricci-flow machinery. Compressing a project of this scope into weeks of AI-assisted formalization demonstrates that frontier formal-mathematics agents can now operate over extensive prerequisite libraries rather than only isolated olympiad theorems or short research arguments. The near-simultaneous second formalization reinforces the historical signal while also discouraging a simplistic single-project priority claim.
Significance rationale: FrenzyMath's Poincaré development is a field milestone in AI-assisted formalization because it packages a complete smooth/topological Poincaré proof route into a multi-million-line Lean project and reports completion of most of the work within roughly half a month using agentic pipelines and publicly available commercial language models. The project exposes a Mathlib-facing statement, full-build evidence and Comparator/Nanoda verification. A separate team released another complete Lean development essentially concurrently, showing that research-scale geometric-analysis formalization had moved from an isolated demonstration to a reproducible frontier. Because the mathematical theorem was already known and the exact agent/human division is not reconstructed theorem by theorem, H2 is more appropriate than H1.
—
—
FrenzyMath's announcement and repositories expose the endpoint statements, proof library, full-build instructions and Comparator/Nanoda verification records. Chronicle has not independently replayed the artifact in this maintenance pass, so machine_checked records the released verification surface rather than an independently_replayed status.
No corrections recorded.
