AI-Assisted Formalization of the Poincaré Conjecture

Summary (Overview)

• The paper reports the first complete Lean 4 formalization of the Poincaré conjecture (both topological and smooth versions), following Morgan–Tian's exposition of Perelman's proof via Ricci flow.
• The project used a milestone-based workflow: 90 reviewed milestone statements served as stable interfaces, enabling parallel AI-agent work and targeted human mathematical intervention.
• The main formalization phase was completed in slightly more than two weeks (after months of preparation) using publicly available commercial models, at a cost of approximately $25,000 (AI subscriptions + server rentals).
• The initial development contained ~3.2 million lines of Lean code; dependency extraction reduced this to ~2.8 million lines while preserving verification.
• The paper analyzes human intervention patterns, compares with the FLT formalization, and discusses the path toward reusable geometric-analysis infrastructure in Lean.

---

Introduction and Theoretical Foundation

The Poincaré Conjecture

Every simply connected, closed three-manifold is homeomorphic to the three-sphere.

Proved by Perelman (2002–2003) via the Ricci flow program initiated by Hamilton. The proof requires substantial geometric analysis—Riemannian geometry, Ricci flow, geometric limits, surgery, and three-manifold topology—for which Mathlib (Lean's community library) lacked mature reusable interfaces at project start.

Related Work

• Lean 4 and Mathlib: Proof assistant where mathematics is formulated as code; kernel checking guarantees soundness. Mathlib lacked much required infrastructure for geometric analysis.
• Autoformalization: Early work focused on statement translation; later, language models generated formal proofs. Agent systems use library retrieval, compiler feedback, and repeated task execution.
• FLT formalization (September 2026, using Prove2Me): Complete computer-checked proof of Fermat's Last Theorem at unprecedented scale, but with less detail published about human–AI division of labor.

Key Challenge

The proof requires geometric analysis for which no mature formal infrastructure existed—so building foundations was an essential part of the project, not just formalizing an existing proof.

---

Methodology

Workflow Overview

The project proceeded in two phases:

1. Preparation (May–August 2026): Source collection, initial formalization attempts (e.g., Hopf–Rinow theorem), natural-language proof blueprint following Morgan–Tian.
2. Main formalization (September 2026, ~2 weeks): Redesigned workflow based on 90 milestones.

Milestone Structure

Each milestone specified:

• A Lean statement (target theorem)
• Required definitions
• Dependencies (which earlier results it uses)
• Completion conditions

This structure enabled:

• Parallel agent work on independent dependency chains
• Mathematical review of statements before/while formalization (two-pass review: written definitions vs. elaborator output)
• Blocker localization—identifying whether failures were mathematical gaps, Lean implementation problems, or coordination issues

Agent Execution

Two complementary modes:

1. Interactive coding-agent sessions (Codex, Claude Code): Tightly scoped, high-context interventions with a "proof-branch harness" fixing boundaries, endpoints, interfaces, and sources.
2. Archon Horizon (distributed control plane): Bounded missions with explicit goals/dependencies, dispatched to agents on different servers for parallel execution.

Model Division of Labor

• GPT-6-Astra: Main statement formalization and proof construction
• Fable-5.1: Independent source-alignment checks, diagnosis of blocked branches, refinement

Project Resources

---

Empirical Validation / Results

Key Results

• Full Lean build passes with Comparator verification against target statements written using only Mathlib.
• Both topological and smooth Poincaré theorems are proved.
• Initial development: ~3.2 million lines of Lean code; reduced to ~2.8 million via dependency-cone extraction.

Mathematical Bottlenecks and Interventions

Three recurring classes of human intervention were identified:

1. Scope setting (M22): The noncollapsing argument was formulated in dimension three, while an auxiliary result about asymptotic volume ratios retained general dimension to support induction on dimension.

2. Proof-route diagnosis (M28): A curvature estimate for singularity analysis required a local limiting construction not supplied by the available compactness theorem. Mathematicians identified the missing local compactness argument and geometric contradiction, turning an apparent theorem-application failure into explicit supporting tasks.

3. Interface correction and reusable output (M64–M65): Review of the annulus comparison required an explicit initial annulus connecting boundary loops—equal winding around an auxiliary circle was insufficient. The task was strengthened to retain polygonal approximations with error/area bounds for downstream reuse.

Comparison with FLT Formalization

---

Theoretical and Practical Implications

On Workflow Design

"The organization of the formalization process was as important as the capabilities of the underlying agents."

Key findings:

• Fixed, reviewed statements constrain agent work around correct mathematical targets
• Localizing failures via milestones makes blockers diagnosable (mathematical vs. implementation vs. coordination)
• Review timing matters: reviewing statements before formalization (not after) prevents accumulation of locally-successful proofs around unsuitable definitions

On Reusable Infrastructure

• ~48% of the Lean source is background theory and shared mathematical infrastructure
• Example: Smooth structures on compact connected topological three-manifolds span ~650,000 lines, though Morgan–Tian invokes this in a footnote
• The current development is not finished: plans include removing duplication, improving documentation, generalizing definitions, and contributing selected components to maintained libraries (e.g., TauCeti)

On Mathematical Discovery

Formalization can reveal mathematical corrections and simplifications:

• A separate Laver-function project identified corrections incorporated into a revised paper
• The Poincaré formalization revealed potential mathematical revisions that could simplify parts of the argument

---

Conclusion

Main Takeaways

1. An independent research team achieved large-scale formal verification of a major theorem through human–AI collaboration using publicly available models.
2. The milestone-based workflow—with mathematician-reviewed statements as stable interfaces—was the critical organizational innovation enabling parallel agent work and effective human oversight.
3. The project provides a verified proof and a checked source from which a maintainable geometric-analysis library can be developed.

Future Directions

• Refactor the development into a reusable geometric-analysis library (review interfaces, remove duplication, improve organization)
• Analyze agent proof paths for alternative arguments or mathematical observations worth recording independently
• Refine the proof blueprint into a clearer mathematical account with explicit dependencies
• Reduce formalization cost as models improve, enabling independent mathematicians to verify their own research
• Build community infrastructure: libraries, tools, and practices for human–AI interaction centered on Lean

Invitation

"We invite mathematicians to carry their high-level mathematical knowledge into human–AI interactions centered on Lean, and to help build the libraries, tools, and practices this development requires."

---

Repository: https://github.com/frenzymath/PoincareConjecture
Website: https://frenzymath.github.io/Poincare-Conjecture/#/