Background
Poincaré stated his conjecture in 1904. Perelman posted three preprints in 2002 totaling under 70 pages; top mathematicians then spent three to four years verifying them page by page, writing over 500 pages of monographs (notably Morgan–Tian) to fill in skipped steps.
On September 29, 2026, two teams that did not know of each other announced the same day that this proof路线 had been fully written into Lean:
- A team at Peking University's Beijing International Center for Mathematical Research, publicly known as FrenzyMath.
- A team led by Bennett Chow (UC San Diego), posted as arXiv:2609.33842 (submitted September 27), authored by Ziyang Qin, Yuan Liao, Ayush Khaitan, and Bennett Chow.
- The US team's repository is ~4.7 million lines, all passing Lean's kernel check with no
sorry. Tracing citations back from the final Poincaré theorem, the actually used code is 14,197 files / ~4.02 million lines; the longest citation chain spans 353 files. - Code corresponding to Perelman's three papers is ~660,000 lines — only one-sixth. Paper three is 7 pages, averaging ~14,000 lines per page; the curve-shortening flow mentioned in one sentence became 76,000 lines of Lean.
- The remaining five-sixths is material the papers assume readers know: analysis (~1.09M lines), differential geometry (~770K lines), and Moise smoothing (topological → smooth manifolds, 460K lines). The heaviest piece is the canonical neighborhood theorem, supporting 2.72 million lines — two-thirds of the dependency chain; the DeTurck trick alone (turning Ricci flow under coordinate change into a standard heat equation) requires 890K lines.
- PKU's accounting: half a month, under $30,000 including LLM API calls and server costs — under one cent per line. In March, their in-house Archon system formalized a research-level problem in ~8,800 lines over 50 hours for $1,200 (~$0.14/line). Per-line cost has fallen to about a tenth of that in half a year.
- At an estimated 250 lines/day per human expert (250 workdays/year), 3.2M lines would take one person 50 years; half a month equates to 800+ formalization experts working simultaneously.
- The core team: 3 AI developers with math backgrounds, plus postdocs and PhD students. They don't hand-write code; they build agent workflows: a human-readable blueprint listing 279 definitions/theorems in six chapters with book references, plus 16 supporting blueprints from textbooks and papers. In mid-August, 11 "borrowed for now" IOUs remained in the blueprint; by the September 28 delivery, no
sorryand no extra axioms. - Not: "AI independently proved the Poincaré conjecture." Both teams formalized existing human proofs; no new mathematics was produced.
- Worth watching: the price curve. Verifying a Millennium Problem once took the field's top minds three to four years; now it's half a month and $30,000 — affordable to a single lab. [Inference] Tao has described this shift as from proof scarcity to proof abundance; this round's scale and cost put concrete numbers on it.
- Also worth watching: the cost of foundations. Both teams rewrote large chunks of analysis and differential geometry because Mathlib lacked them. Whether this code flows back into the common library determines whether the next formalization keeps getting cheaper — or is repeated from scratch. [Judgment]
- Sources: coverage of the PKU team (Sept 29), coverage of the UCSD team, arXiv:2609.33842 (submitted Sept 27), AGI Hunt daily (Sept 29)
- Caveat: the Collatz and Thomson items currently rest only on team self-reports and secondhand retellings, without peer review; listed here as leads only.
Scale: one-sixth Perelman, five-sixths omitted foundations
The PKU repository has 27,203 Lean files; code referenced by the two final Poincaré theorems totals ~2.9 million lines with over 76,000 theorems/lemmas, organized into 83 milestones from a blueprint. The largest, M76 (~650K lines), does the same job as the US team's 460K-line Moise bridge. Perelman's famous surgery took ~470K lines; finite-time extinction ~390K lines. Their shared library, Horizon, is ~840K lines, nearly 40% general Ricci flow theory.
Both independent teams converged on the same most expensive spot.
| Item | PKU FrenzyMath | UCSD team | |---|---|---| | Total size | ~3.2M lines | ~4.7M lines | | Cited by final theorems | ~2.9M lines | ~4.02M lines | | Files | 27,203 | 14,197 (in chain) | | Perelman original | surgery ~470K lines | ~660K lines total | | Topology→smooth bridge | M76, ~650K lines | Moise, 460K lines | | Organization | 83 milestones + blueprint | dependency chain + ad-hoc agents | | Public ID | team announcement | arXiv:2609.33842 |
Machine-reviewing a book: A.19 didn't pass
Formalizing the Morgan–Tian monograph means re-examining every sentence. A PKU review document (August) found that Appendix A.19 stated, unconditionally, that a 3D space made entirely of "necks" must be a tube. The review refuted this in one line: glue a tube end-to-end into a loop — every point still looks like a neck, but it is not a tube. That loop is S²×S¹. The team dropped A.19 in favor of the adjacent A.20, restated as "either a tube or a loop."
Even mathematicians' intuitive commonplaces had to be re-proven for the machine: the Jordan curve theorem took over 3,000 lines; the Schoenflies theorem (the interior is exactly a disk) took 116,000 lines.
$30,000, under a cent per line
Workflow: blueprint → 83 milestones → agents write lemmas → Lean build → Comparator grading → nanoda secondary kernel re-check.
Who signs off
PKU delivered the first version passing both Lean compilation and Comparator, Lean's official grading tool (problem statement must match exactly, only three standard axioms, kernel-verified step by step). An independently implemented kernel, nanoda, re-graded the entire proof — the same dual-kernel approach Anthropic used for the 13-million-line Fermat's Last Theorem formalization.
One nuance: a formalized proof guarantees the formal derivation has no gaps; whether the formalization is *faithful to Perelman's original proof* rests on blueprints, human review, and citation-chain tracing. PKU catching the A.19 error suggests this layer was genuinely done, not rubber-stamped. [Judgment]
What to watch — and what not to
Same-day smaller items: Lech Mazur announced a Codex-based agent result giving a new Collatz conjecture lower bound (for large X, at least cX positive integers n < X return to 1 within 10.46 ln(n) steps, a nonzero proportion; prior best bounds were X^0.84 and X^0.90), with Lean formalization completed; Vals AI reported 10 Claude Sonnet 5.5 agents generated a 17,895-line Lean proof of the Thomson problem N=7 in ~15 hours, concluding the minimum-energy arrangement of seven charges is a pentagonal bipyramid.