Perelman's proof of the Poincaré conjecture formalised in Lean, with AI-generated code (Chow, Qin, Liao, Khaitan)
On Sept 27, 2026 Ziyang Qin, Yuan Liao, Ayush Khaitan and Ricci-flow expert Bennett Chow posted a Lean 4 formalization of the Hamilton–Perelman proof of the 3D Poincaré conjecture. Via the Moise smoothing theorem it covers both the smooth and the topological versions, and it proves the statement Mathlib had marked `proof_wanted`. The axiom check shows no `sorry` and no project axioms. The paper says "automated assistance was used for proofs and prose". Secondary reports say about 2.7M of 4.7M Lean lines were produced in the last two weeks with ChatGPT/Codex and Claude. It is the first machine-checked proof of a solved Millennium Prize problem.
Key facts
- arXiv 2609.33842 (math.DG), submitted Sept 27, 2026; code: github.com/qinz1yang/differential-geometry, release v0.1.3 (Lean/Mathlib v4.33.1)
- Lean endpoints: exists_isManifold_three (Moise), smoothPoincareConjecture_holds (smooth), DifferentialGeometry.Topology.poincare_conjecture (topological); all four queried closures use only propext, Classical.choice, Quot.sound, with no sorryAx or project-specific axiom (paper)
- Proves the topological 3D Poincaré statement marked proof_wanted in Mathlib v4.33.1, checked by applying the endpoints directly (paper)
- Route: Ricci flow with surgery and finite-time extinction (Hamilton–Perelman), following Kleiner–Lott and Morgan–Tian
- AI disclosure in the paper: 'Automated assistance was used for proofs and prose; the authors retain responsibility'; it reuses parts of Tau Ceti, a Lean library credited to 'J. Tooby-Smith, Codex, and The Tau Ceti contributors'
- Secondary report (KuCoin flash citing Chinese outlet Xinzhiyuan): ~4.7M lines in total, ~2.7M in the final two weeks with ChatGPT (Astra), Codex and Claude (Fable 5.1); Qin made 7,477 of 11,000+ commits; ~7 months of work. Unverified against a primary source
- Preceded by the same group's 'A Lean Formalization of Hamilton's Three-Manifold Theorem' (arXiv 2608.21502, Aug 2026); a separate Frenzymath/PKU Poincaré project is in progress
Science result
- Field
- mathematics / geometric topology / Ricci flow / formal verification
- Problem
- Formal verification of the Poincaré conjecture (Clay Millennium Prize problem, solved by Perelman 2002–03) (open since 1904)
- Result
- Complete Lean 4 formalization of the smooth and topological 3D Poincaré conjecture via Ricci flow with surgery, with no sorry or extra axioms.
- AI system
- Codex, ChatGPT (GPT-6 Astra, reported), Claude (Fable 5.1, reported)
- Human role
- Human-led (Chow's group) with heavy AI code generation; the paper discloses automated assistance for proofs and prose
- Verification
- Formal proof in Lean (kernel-checked; definitions still need human review)
- Status
- pending
- Why surprising
- A proof once considered among the hardest to check, which took experts years to verify, was machine-checked within months by a four-person team leaning on AI coding agents.
What happened
Bennett Chow (UCSD), a leading Ricci-flow researcher, and three younger collaborators released a Lean 4 library that formalizes the whole Hamilton–Perelman proof: short-time existence via DeTurck, singularity analysis, surgery and finite-time extinction. With the Moise smoothing theorem it yields the topological Poincaré conjecture. The paper is short (it points to the code) and includes axiom-check commands that anyone can rerun.
The paper discloses AI help in one sentence. The scale (millions of lines in months) and the model names come from secondary reports, and confidence is medium until the authors or the labs confirm them.
Why it matters
After Fermat's Last Theorem (Claude, Sept 2026), this is the second landmark formalization of a famous proof in a month. Perelman's proof needed years of expert refereeing in 2003–06. A kernel-checked version suggests that AI-generated Lean at scale now reaches the hardest parts of geometric analysis. Experts still have to check that the Lean definitions match the mathematics.
Changelog
- 2026-10-01: created (leads run, 07:40 completion)
Related events
- Claude produces the first complete machine-checked proof of Fermat's Last Theorem in Lean, in 11 days ★★★★★
- Math Inc's Gauss formalises Viazovska's sphere-packing proofs in dimensions 8 and 24, fixing errors in the originals ★★★★
- Lean Pool: an AI-maintained archive of Lean formalizations grows past 3 million lines ★★
- OpenAI claims a Millennium Prize problem: 10,000 AI agents prove forced Navier–Stokes blow-up; priority dispute erupts ★★★★★
- Mistral releases Leanstral 1.5, an open-weights Lean 4 proof agent that saturates miniF2F and solves 587/672 PutnamBench problems ★★★
Sources (6)
- paperarXiv: A Lean Formalization of the Hamilton–Perelman Proof of the Three-Dimensional Poincaré Conjecture
- codeGitHub: qinz1yang/differential-geometry
- paperarXiv: A Lean Formalization of Hamilton's Three-Manifold Theorem (2608.21502)
- pressKuCoin News: Poincaré Conjecture proof fully verified by AI in 4.7 million lines of code
- discussionBennett Chow: Ricci Flow as a Test for AI (CMSA talk slides, Sept 2025)
- codeFrenzymath: Formalizing the Poincaré Conjecture in Lean 4 (separate project)
id: 2026-09-27-poincare-conjecture-lean-formalization · updated 2026-10-01 · open in the interactive timeline