Breakthrough Tracker record
A Lean development claims to formalize the Hamilton–Perelman proof of 3D Poincaré
Qin and collaborators released a Lean 4 development claiming to formalize the smooth three-dimensional Poincaré theorem, Moise smoothing and the topological endpoint through Ricci flow with surgery and finite-time extinction.
← Back to the filtered Breakthrough Tracker
- Stable ID
math-poincare-lean-formalization-2026- Revision
math-poincare-lean-formalization-2026.v3- Field
- Mathematics · Formal methods, differential geometry and Ricci flow
- Evidence
- Tier 1 · Peer reviewed: No
- Record state
- Provisional · Released formalization claim
- Last checked
AI role
The paper reports automated assistance for proofs and prose without quantifying it; the named authors retain responsibility.
Record details
- Problem or result
- Lean formalization of the Hamilton–Perelman proof of the three-dimensional Poincaré theorem
- Authors
- Ziyang Qin, Yuan Liao, Bennett Chow and Ayush Khaitan
- Institutions
- Cornell University; University of California, San Diego; Princeton University and Princeton Language and Intelligence
- Result date
- Paper submitted September 27; reviewed stable release v0.1.4 on October 5; development preview v0.1.5 on October 9, 2026
Why it matters
If its definitions and interfaces withstand expert audit, this is an unusually large formal-verification milestone for modern geometric analysis.
Limits
Poincaré was not newly proved. Stable v0.1.4 remains the last tracker-reviewed source. The newer v0.1.5 development preview adds claimed geometrization and Mostow–Prasad work but explicitly awaits later integration and build caches. A successful kernel build does not establish that every formal definition matches the intended geometry; independent semantic review remains pending.
Sources
- Primary: Qin et al., formalization of the 3D Poincaré theorem
- Formal proof: Stable v0.1.4 Lean source release
- Formal endpoint: Pinned v0.1.4 topological Poincaré endpoint
- Release record: DifferentialGeometry stable release v0.1.4
- Development preview: DifferentialGeometry v0.1.5 preview release
- Independent formalization claim: Zhang and collaborators Poincaré formalization preprint
- Independent artifact: Second-team Poincaré Lean repository
Correction and revision history
- 2026-10-02 — Added after primary-source, scope, status, AI-role and limitation review.
- 2026-10-05 — Replaced the v0.1.3 preview pins with stable v0.1.4 and retained the formalization-claim status pending independent semantic review.
- 2026-10-19 — Added the v0.1.5 development preview and a separately assembled Lean project without replacing the reviewed v0.1.4 stable pin or upgrading the semantic-validation claim.
Machine-readable: JSON v1 · CSV v1 · Schema v1
This individual record remains noindex until a story-specific featured image passes Kingy’s rendered-pixel visual review. The source-linked tracker hub remains the public index.