Formalization of the Poincaré Conjecture

The Poincaré Conjecture, one of the seven Millennium Prize Problems, was first posed by Henri Poincaré in 1904:

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

In dimension three, by Moise’s theorem, homeomorphic is equivalent to diffeomorphic.

Intuitively, it states that any closed 3-dimensional shape sharing the sphere’s property, that every loop can be shrunk to a point, can be smoothly deformed into the 3-dimensional sphere.

Between 2002 and 2003, building on Richard Hamilton’s earlier work on the Ricci flow, Grigori Perelman posted a highly compressed and sketchy proof of the Poincaré Conjecture in three preprints with fewer than 70 pages in total. Several groups of mathematicians then worked to fill in the missing details and make the arguments rigorous and complete. One such effort was by John Morgan and Gang Tian, who wrote a book of more than 500 pages to expand the details, clarify the exposition, and make the proof precise. Our formalization mainly follows the Morgan–Tian exposition of Perelman’s proof.

Formalization can be seen as the ultimate form of this mathematical practice: expanding every proof detail down to the lowest level and mechanically verifying the absolute correctness of each argument. Previously, this process was slow and required substantial human effort. In our work, we completed the main body of the formalization in Lean 4 in half a month. The effort brought together three AI developers with mathematical backgrounds, who designed, built and ran the agentic pipelines, and several volunteer mathematicians, all working with publicly available commercial large language models. It produced about 3.2 million lines of code, at a total cost of less than $30,000 for LLM usage and compute servers. The proof rests primarily on Riemannian geometry and differential geometry, but also draws on broader fields such as topology and partial differential equations. Much of the foundations in all these areas had not yet been formalized, requiring all prerequisite theory to be formalized within this project.

Formalizing the Poincaré Conjecture signals the beginning of a new era in formalization: large-scale formal verification of proofs built on extensive theoretical foundations, such as those of the Millennium Prize Problems and, as another landmark example, Anthropic’s formalization of Fermat’s Last Theorem², can now be completed in a relatively short time and at a cost affordable to some academic institutions, but not yet cheap enough to be accessible to everyone.

The accessibility of formalization matters because AI now helps produce far more proofs than ever, making verification more necessary than ever. Much further reductions in cost are needed to make verification of all new proofs feasible. This in turn calls for reusable infrastructure that shortens the distance from existing formalization to frontier proofs. Such libraries would save future projects from the foundation-building this one required. Our current code quality is still far from achieving this. We envision a future in which formalization is accessible to everyone and becomes part of daily mathematical practice, helping mathematicians check their own work³, clarify details, fix errors, and sharpen definitions in near real time, while greatly accelerating review. We pursue this future and are committed to continuing to improve the quality of our current code, as future work, toward building reusable, high-quality infrastructure.

More details will be shared in a blog post soon.