A four-person team has written a fully machine-checked formalization of the Poincare conjecture proof in Lean, turning one of mathematics’ best-known results into code that the system’s kernel can verify.
According to the report, the project covers about 4.7 million lines of code. Roughly 2.7 million of those lines were produced in the final two weeks with help from AI systems including ChatGPT and Claude. The full codebase passed Lean kernel checks, and none of it was left with a "sorry" placeholder for unfinished arguments.
Millions of lines behind the final theorem
The report says that tracing direct and indirect dependencies from the final Poincare theorem leads to 14,197 code files and about 4.02 million lines of code. The longest dependency chain runs through 353 files.
Code corresponding to Grigori Perelman’s three papers totals about 660,000 lines, or roughly one-sixth of the whole. The shorter the original paper, the more Lean code had to be supplied to fill in omitted steps. In the third paper, which runs just seven pages, the average comes to about 14,000 lines per page. A curve-shortening flow argument mentioned in a single sentence there expands to 76,000 lines in Lean.
The remaining five-sixths consist largely of background mathematics that the papers take for granted. The report puts analysis at about 1.09 million lines and differential geometry at about 770,000 lines.
Ricci flow and the heaviest parts of the dependency chain
Ricci flow is the central tool in Perelman’s proof. The report describes it as a process that gradually smooths out highly curved regions of a space, in a way comparable to heat diffusion.
One basic result is short-time existence: given an initial shape, Ricci flow can at least run forward for a short interval. But the Ricci flow equation changes form under a change of coordinates, so it is not a standard heat equation. In 1983, DeTurck introduced a method that adds a term to convert it into a standard heat equation and then transforms the solution back. In Lean, the Sobolev spaces, spectral theory, and other tools behind that method all had to be formalized. The report says this single theorem draws on 890,000 lines of code.
Perelman’s decisive tool is the canonical neighborhood theorem. It says that regions where curvature is about to blow up in Ricci flow must have a controlled local shape, either a neck or a cap. Formalizing that theorem requires 2.72 million lines of code, according to the report, or about two-thirds of the full dependency chain.
The researchers and the AI workflow
The team is led by Ben Chow, a mathematics professor at the University of California, San Diego. The report says Chow earned his PhD at Princeton in 1986 under Shing-Tung Yau. It also recounts that shortly after Richard Hamilton introduced Ricci flow, Yau pointed out that the flow would pinch thin parts of a space apart, which could be the first step toward a proof. Hamilton later recalled that exchange.
In the fall of 2025, Chow and collaborators started an online Lean study group and learned the system from the ground up. At the time, the report says, Mathlib still lacked some of the most basic tools for Riemannian geometry. Chow, Ziyang Qin, and UCSD PhD student Yuan Liao then spent seven months building about 2 million lines of foundational code.
Qin, described in the report as the undergraduate who pushed at the front of the effort, graduated from Cornell in May and had not yet started a PhD. Out of more than 11,000 repository commits, 7,477 were under his name. In September, Princeton’s Ayush Khaitan joined with topology tools, and the four researchers completed the final two-week sprint together.
The report names ChatGPT Astra as the main AI system used, with Claude Fable handling some of the harder sections. In the open-source toolkit described by the team, the top layer on the AI side is a lead session that the researchers talk to directly. That lead session does not write proofs itself; it keeps the mathematical route on track. Beneath it sits a long-running scheduler agent that breaks work apart, assigns tasks, and reviews submissions. The actual proof writing, debugging, and reference checking are handled by temporary agents that exit after finishing a single job. Human authors remain above the whole stack, choosing definitions, setting statements, and confirming that what Lean proves is the statement mathematicians actually want.
The September sprint
During the sprint, the team was formalizing the topology portion section by section from a textbook published by topologist Edwin E. Moise in 1977.
On the morning of Sept. 20, Claude Fable 5.1, acting as the lead, wrote a task sheet that split the work into four parallel tracks and handed them to OpenAI’s coding agent Codex. Each track was allowed to edit only its own files, then return a checklist for Claude to review before submission.
One rule mattered above all: the team would not weaken a statement just to make it provable. If a statement turned out to be false, that still counted as a successful outcome, and the system was supposed to stop and report a counterexample.
Later that evening, the lead agent produced a revised schedule. With three to four parallel tracks, the hardest sections of the book were expected to take six to 10 weeks, and reaching the topological version of the Poincare theorem would still take more than four months at best.
Half an hour later, the human lead chose a different approach: build the skeleton first. That meant laying out the structure of the proof, using sorry placeholders for steps that could not yet be proved, exposing interface mismatches early, and then reviewing, finalizing, and proving each placeholder statement one by one. Those skeleton files were stored separately and never entered the main repository, so the finished codebase still contains no sorry at all.
On Sept. 23, Ben Chow’s side completed three pieces in Section 32, with the Claude lead handling review. Only after compilation and audit returned zero errors was the work merged into the main repository. The next day, a chain of theorems from Sections 25.2 through 34.1 was completed. At 3:38 a.m. Eastern Time on Sept. 27, the topological version of the Poincare theorem was finished, less than a week after that schedule had been drawn up.
The conjecture and the surgery method
The Poincare conjecture was posed in 1904. It states that if a finite, closed three-dimensional space has the property that every loop can be contracted to a point, then the space is a three-sphere.
The problem remained open for nearly a century. Higher-dimensional versions were solved much earlier, but the three-dimensional case resisted. That changed in late 2002 and 2003, when Perelman posted three papers on arXiv and broke through using Ricci flow.
The basic idea is to smooth a space out over time. If the space can be made uniformly round, then it is a sphere. The difficulty is that the flow can develop singularities. The report uses a dumbbell picture: two large balls connected by a thin rod. As Ricci flow runs, the rod gets thinner and thinner until it pinches off in finite time. Curvature at the pinch point blows up to infinity, creating a singularity.
Hamilton was stuck at that stage for years. Perelman’s canonical neighborhood theorem identified the only local shapes that can appear near trouble spots, necks and caps, and that made surgery possible. The method cuts through the middle of a neck before the pinch forms, removes the dangerous segment, caps off the two new ends with standard pieces, and lets Ricci flow continue.
A 23-line theorem file built on top of millions of lines
Perelman’s third paper also proved that for simply connected spaces, repeating the cycle of flowing, performing surgery, and flowing again makes the whole space shrink away in finite time. Each disappearing component is a three-sphere, and gluing them back together along the surgery cuts still gives a three-sphere.
Many key steps in the three papers were originally stated without full detail. The report notes that only in 2006, after several groups of mathematicians wrote detailed accounts running hundreds of pages, did the field accept the proof as secure.
In this repository, the roughly 4.02 million lines of supporting code ultimately serve a theorem file that is only 23 lines long. The theorem states that every compact, simply connected, boundaryless three-dimensional topological manifold is homeomorphic to the three-sphere.
Because Ricci flow runs only on smooth spaces, the formalization also needs Moise’s theorem as a bridge. Moise proved in 1952 that every three-dimensional topological manifold can be triangulated and then smoothed, giving it a smooth structure. The second half of that 23-line file first uses Moise’s theorem to obtain a smooth structure and then invokes the smooth version of the Poincare conjecture.
The report says that this bridge is even more code-heavy than the surgery portion. The PL topology code responsible for it runs to 460,000 lines, nearly twice the size of the surgery section. Responding to a question about why the last lines could not simply call the smooth Poincare theorem directly, Khaitan said parameters C and hC could not be omitted because Lean first has to verify that the manifold carries a smooth coordinate structure, and those parameters come from Moise’s theorem.
From 25,000 lines to 4.7 million
The report compares the project with Gauss, an automatic formalization agent that wrote 25,000 lines of code in three weeks a year earlier and already drew wide attention. This time, four researchers and a group of AI systems produced more than 100 times that amount in two weeks.
Stanford mathematician Jared Duker Lichtman reacted by reposting the news with two exclamation marks. The division of labor described in the report points to a different research workflow: senior mathematicians set direction, younger researchers work line by line with AI, and Lean’s kernel decides whether the proof goes through. In that setup, more of the human role shifts from writing every step by hand to deciding what should be proved and catching places where AI gets the mathematics wrong.
The source article cites reference materials including Ayush Khaitan’s posts on X, the qinz1yang/differential-geometry repository and its pull request, an arXiv paper, the auto-formalizing-skills repository, Ben Chow’s LeanOnMe page, Keith Adler’s X post, and a math.inc page on Gauss. The original piece was credited to the WeChat public account "新智元" (ID: AI_era) and authored by "ASI启示录."