# An AI-Assisted Formalization of the Poincaré Conjecture

> The Poincaré conjecture was fully formalized in Lean 4 in two weeks for $25,000 using AI agents guided by 90 mathematician-reviewed milestones as stable interfaces.

- **Source:** [arXiv](https://arxiv.org/abs/2610.08329)
- **Published:** 2026-10-17
- **Permalink:** https://picx.dev/p/1swrmE
- **Whiteboard:** https://picx.dev/p/1swrmE/image

## Summary

# 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

| Resource | Cost |
|----------|------|
| AI subscriptions (GPT Pro 20× plans) | ~$20,000 (~100 subscriptions at $200 each) |
| Linux server rentals (Lean compilation) | ~$5,000 |
| **Total** | **~$25,000** |

---

## 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

| Aspect | Poincaré | FLT |
|--------|----------|-----|
| Foundation | Project-specific infrastructure needed (geometry, Ricci flow, surgery) | Built on Mathlib + existing FLT projects |
| Workflow | 90 pre-reviewed milestones from Morgan–Tian route | Prove2Me DAG of statements, statements separated from proofs |
| Key shared principle | Explicit dependencies + fixed statement interfaces | Explicit dependencies + fixed statement interfaces |
| Early attempts | Failed; restart needed | Failed; agents lost track of project state |

---

## 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/#/*

---

_Markdown view of https://picx.dev/p/1swrmE, served by PicX — AI-generated visual whiteboard summaries of research papers._