Poincaré Conjecture proof fully verified by AI in 4.7 million lines of code

Just now, the complete proof of the Millennium Prize problem, the Poincaré conjecture, was written entirely in code!

A small team of just four people accomplished this.

Leading the charge was a senior professor who had spent decades researching Ricci flow, a disciple of Shing-Tung Yau; at the very front was a recent undergraduate graduate, followed by a team of AI systems working around the clock.

They used the proof assistant Lean to rewrite the entire proofs by Hamilton and Perelman, totaling approximately 4.7 million lines of code.

Approximately 2.7 million lines were completed in the last two weeks with the help of AI tools such as ChatGPT and Claude.

These 4.7 million lines have all been verified by the Lean kernel, with no instances left using "sorry" to defer proof for later.

In the past, getting the mathematical community to say “no issues” on a large proof required peers to spend years carefully reviewing it page by page.

This time, the machines are in charge, and AI has become the primary tool for generating proofs.

We downloaded the entire repository and traced all the directly and indirectly referenced code leading to the final Poincaré theorem.

A total of 14,197 code files, approximately 4.02 million lines, were actually used, with the longest reference chain linking 353 files.

Among them, the code corresponding to Perelman's three papers totals approximately 660,000 lines, accounting for only one-sixth.

The more concise the paper, the more code needs to be added in Lean; the third paper, at seven pages, averages 14,000 lines per page.

In the third section, the concept of curve shortening flow—where a curve simultaneously shrinks and becomes circular—is mentioned in just one sentence, but in Lean, it spans 76,000 lines of code.

The remaining five-sixths consist entirely of foundational mathematics that Perelman assumed readers already understood, including approximately 1.09 million lines of analysis and 770,000 lines of differential geometry.

The Ricci flow was the central tool in Perelman's proof, gradually smoothing out highly curved regions of space, much like the principle of heat conduction.

Short-time existence is a classic example. It states that, given any initial shape, the Ricci flow can proceed for at least a short period of time, and the paper only needs to cite a previous result.

The Ricci flow equation changes its form when described in a different coordinate system and cannot be considered a standard heat equation.

In 1983, DeTurck came up with a method: first add a term to the equation to transform it into a standard heat equation, solve it, and then transform it back.

In Lean, all the underlying tools—such as Sobolev spaces and spectral theory—must be built from scratch, and just this single theorem requires 890,000 lines of code.

Perelman's trump card was the canonical neighborhood theorem.

It says that in the Ricci flow, regions where the curvature is about to approach infinity must have a very regular shape.

Either a long, slender tube called the "neck," or a tube with one end sealed, called the "cap."

Proving this theorem requires 2.72 million lines of code, accounting for two-thirds of the entire dependency chain.

Ben Chow, the leader, is a professor of mathematics at UCSD. In 1986, he earned his Ph.D. from Princeton University, with Shing-Tung Yau as his advisor.

Shortly after Hamilton introduced the Ricci flow, Yau Shing-Tung pointed out to him that the flow would pinch off at narrow regions of the space, which might be the first step in the proof. Hamilton later recalled this incident specifically.

He later co-authored papers with Hamilton and wrote a comprehensive series of monographs on Ricci flow, dedicating decades to this field.

In that era, Shing-Tung Yau strongly supported the path of the Ricci flow; forty years later, it was his student who led the team to fully formalize the proof of this approach in a computer.

In the autumn of 2025, this seasoned veteran of geometry, along with his peers, launched an online Lean learning course, approaching the new tool like a beginner and learning from scratch. To this day, his personal homepage features a section titled “Some of My Naive Ideas.”

At that time, Mathlib did not yet have even the most basic tools for Riemannian geometry.

Thus, Chow, Ziyang Qin, and UCSD PhD student Yuan Liao spent seven months writing approximately two million lines of foundational code.

The undergraduate leading the charge is Ziyang Qin. He graduated from Cornell just this past May and hasn’t even started his Ph.D. yet—out of over 11,000 commits in the repository, 7,477 are under his name.

In September, Ayush Khaitan from Princeton joined with topological tools, and the four of them completed the final two-week sprint together.

Regarding the specific AIs used, Khaitan revealed that the primary model was ChatGPT Astra, while some challenging sections were handed over to Claude Fable.

According to the team's open-source toolkit, the topmost AI role is the "Lead," the primary conversation channel through which researchers interact; it does not generate proofs but strictly upholds the mathematical pathway.

Under the team leader, a persistent "scheduling" agent runs in the background, responsible for breaking down tasks, assigning them, and reviewing completion. The actual work—writing proofs, identifying errors, and researching—is carried out by temporary agents that exit after completing each task.

Human authors sit at the top of the entire system, responsible for defining concepts and propositions, and verifying that what is proven in Lean is indeed what the mathematicians intended to prove.

During the final push, the team is writing the section on topology section by section, following a textbook published by topologist Moise in 1977.

Early on September 20, Claude Fable 5.1, as the team lead, created a task list dividing this segment into four parallel task lines and assigned them to OpenAI’s coding agent, Codex.

Each task line may only modify files under their own name. After completion, return the checklist for Claude to verify before submission.

Most importantly, never weaken the proposition just to prove it. Discovering that the proposition is false is also a success—once you provide a counterexample, stop and report it.

In the evening, the leader revised the schedule. Estimating 3 to 4 task lines running in parallel, the sections widely regarded as the most difficult in the book would take 6 to 10 weeks, and reaching the topological Poincaré conjecture would take at least four months.

Half an hour later, the human lead decided to try a different approach and start by building the framework.

First, outline the overall structure of the proof, and temporarily use "sorry" to hold the steps that cannot yet be proven, so that interface mismatches are exposed early. Then, review, finalize, and prove each placeholder proposition one by one.

These skeleton files are stored separately and not merged into the main repository, so the final product still contains no "sorry".

On September 23, three components from Section 32 were verified by Ben Chow’s team, with Claude leading the inspection. Only after the compilation and audit returned zero errors was the work submitted by this professor, who has mentored 16 PhDs, merged into the main repository.

The next day, all the theorems from 25.2 to 34.1 in the book were proven. At 3:38 a.m. EDT on September 27, the topological proof of the Poincaré conjecture was completed, less than a week after the schedule had been laid out.

Returning to the Poincaré conjecture itself.

It was proposed by Poincaré in 1904, meaning that in a finite, closed three-dimensional space, if any loop can be shrunk to a point, then it is a three-dimensional sphere.

This problem has dragged on for nearly a century—higher-dimensional versions were solved long ago, but the three-dimensional case has remained stubbornly unsolved.

Until the end of 2002 through 2003, Perelman published three papers on arXiv, resolving the problem using Ricci flow.

The idea of the Ricci flow is to smooth out the space uniformly. If a space can be smoothed in this way to become perfectly round everywhere, then it is a sphere, and the conjecture is proven.

The problem is that the space doesn't necessarily become perfectly round.

Imagine a dumbbell with two large balls at each end connected by a thin bar.

As the Ricci flow begins, the thin rod becomes progressively narrower and snaps abruptly within a finite time. At the point of snapping, the curvature tends toward infinity, which in mathematical terms is called a "singularity."

Hamilton had been stuck at this step for years. Perelman, armed with the canonical neighborhood theorem, knew that the only possible problem areas were the "neck" or the "cap," so he pulled out his scalpel.

The method is to cut open the middle of the neck before the thin tube is about to be severed, and discard the small section that is about to fail.

Then sew a standard-shaped cap onto each of the two boundaries, allowing the Ricci flow to continue.

Time progresses from bottom to top.

In his third paper, Perelman proved that for a simply connected space, repeatedly flowing, performing surgery, and then continuing to flow causes the entire space to shrink to nothing in finite time.

Each piece that disappears is a three-dimensional sphere; when reassembled by gluing along the cut lines, the result is still a three-dimensional sphere.

These three papers listed only the conclusions for many key steps; it wasn't until 2006, when several groups of mathematicians independently published detailed versions totaling hundreds of pages, that the mathematical community confirmed the validity of the proof.

In this repository, the first 4.02 million lines of code ultimately served a single file containing only 23 lines.

The theorem in the document states the Poincaré conjecture: any compact, simply connected, three-dimensional topological manifold without boundary is homeomorphic to the three-dimensional sphere.

The Ricci flow can only operate on smooth spaces, so the Moise theorem is needed to build a bridge.

In 1952, Moise proved that every three-dimensional topological manifold can be decomposed into small tetrahedra, assembled together, and then smoothed along the seams to yield a smooth structure.

The second half of those 23 lines of code does exactly that—“build the bridge before crossing the river”: first use the Moise theorem to obtain a smooth structure, then invoke the smooth version of the Poincaré conjecture.

The Moise bridge was even more challenging than the surgical component. The PL topology code responsible for it—code that studies space by piecing together small fragments—consists of 460,000 lines, nearly double the amount of the surgical component.

A mathematician asked in the comments whether the last few lines could simply be replaced with a single call to the smooth Poincaré version.

Khaitan replied that the parameters C and hC cannot be omitted, because Lean must first confirm that the manifold has a smooth coordinate system. These two parameters are derived from Moise's theorem.

A year ago, it was big news when the automated formalization agent Gauss wrote 25,000 lines of code in three weeks.

This time, four people plus a group of AIs produced over a hundred times more in two weeks.

Stanford mathematician Jared Duker Lichtman added two exclamation marks when sharing.

The division of labor within this team is almost exactly how future mathematical research will look: veterans set the direction, young researchers write code line by line with AI, and the final correctness is determined by Lean’s core.

Human mathematicians are shifting their efforts from writing proofs step by step to deciding what to prove and identifying errors in AI-generated proofs.

At this rate, the next problem AI helps solve might be one that has yet to be proven by anyone.

Reference materials:

https://x.com/ayushkhaitan343/status/2104289939840176167

https://github.com/qinz1yang/differential-geometry

https://github.com/qinz1yang/differential-geometry/pull/80

https://arxiv.org/abs/2608.21502

https://github.com/qinz1yang/auto-formalizing-skills

https://mathweb.ucsd.edu/~bechow/LeanOnMe/

https://x.com/keithadler/status/2104340829401980938

https://www.math.inc/gauss

This article is from the WeChat public account "New Intelligence Yuan" (ID: AI_era), authored by ASI Revelation.