For stock trading, check the Jin Qilin analyst research report: authoritative, professional, timely, and comprehensive, helping you uncover potential thematic opportunities! (Source: Xinzhiyuan) Xinzhiyuan reports that just now, the complete proof of the Millennium Prize Problem, the Poincare conjecture, has been entirely written into code! The team that accomplished this is only a small group of four people. Leading them is a disciple of Qiu Chengtong, an old professor who has studied Ricci flow for decades, while charging at the front is a freshly graduated undergraduate, backed by a group of AIs running around the clock. Using the proof assistant Lean, they wrote the proofs of Hamilton and Perelman from beginning to end, totaling about 4.7 million lines of code. Of that, about 2.7 million lines were rushed out in the final two weeks with the help of AI such as ChatGPT and Claude. These 4.7 million lines have all passed checks by the Lean kernel, with no place left with sorry as "to be proved later."

In the past, for a major proof to earn the mathematical community's verdict of "no problems," peers had to spend years reading it page by page. This time, the arbiter became a machine, and the main force writing the proof also became AI. Perelman's life's work actually accounts for only one-sixth. We downloaded the entire repository and, following the final Poincare theorem, found all the code it directly and indirectly references. What was actually used included 14,197 code files, about 4.02 million lines, and the longest reference chain connected 353 files. Among them, the code corresponding to Perelman's three papers totaled about 660,000 lines, only one-sixth of the total. The more concise the paper, the more code had to be filled in within Lean; the 7-page third paper corresponded to an average of 14,000 lines per page. The curve shortening flow mentioned in only one sentence in the third paper, which makes a curve shorten while becoming round, was written into 76,000 lines in Lean. The remaining five-sixths was all the foundational mathematics that Perelman assumed in his papers "readers already understand," including about 1.09 million lines of analysis and about 770,000 lines of differential geometry. Ricci flow is the core tool of Perelman's proof; it gradually smooths out places in space that are strongly curved, with a principle similar to heat conduction. Short-time existence is a typical example. It says that for any given initial shape, Ricci flow can at least run forward for a short while, and in the paper it only required citing a previous conclusion. But when the Ricci flow equation is described in a different coordinate system, its form changes accordingly, and it cannot be regarded as a standard heat equation. In 1983, DeTurck came up with a method: first add a term to the equation, transform it into a standard heat equation, solve it, and then transform back. In Lean, the tools behind this method, such as Sobolev spaces and spectral theory, all had to be written from scratch, and this one theorem alone required 890,000 lines.

Perelman's killer move is the canonical neighborhood theorem. It says that where the degree of curvature in Ricci flow is about to tend to infinity, the shape must be very regular. Either it is a slender circular tube, called a "neck," or it is a circular tube with one end sealed, called a "cap." Proving this one theorem required 2.72 million lines of code, accounting for two-thirds of the entire dependency chain. Behind the old and the young is AI managing AI. The leader, Ben Chow, is a mathematics professor at UCSD. In 1986, he received his doctorate at Princeton, and his advisor was none other than Qiu Chengtong. Shortly after Hamilton proposed Ricci flow, Qiu Chengtong pointed out to him that this flow would pinch space apart where it is thin, and that this might be exactly the first step of the proof. Hamilton later specifically recalled this. He later coauthored papers with Hamilton and wrote an entire set of monographs on Ricci flow, grinding away in this direction for decades. The person who vigorously supported the Ricci flow path back then was Qiu Chengtong, and forty years later, his student led the team that completely wrote the proof of this route into a computer. In the fall of 2025, this veteran geometer and his peers started an online Lean study group, learning this new tool from scratch like a beginner. His personal homepage still has a column titled "Some of my naive ideas." At that time, Mathlib did not even have the most basic tools of Riemannian geometry complete. So Chow, Ziyang Qin, and UCSD doctoral student Yuan Liao spent seven months first writing about 2 million lines of foundational code. The undergraduate charging at the front is Ziyang Qin. He only graduated from Cornell in May this year, has not even started his doctorate, and of the more than 11,000 commits in the repository, 7,477 are under his name. In September, Ayush Khaitan from Princeton joined with topology tools, and the four completed the final two-week sprint together. As for exactly which AIs were used, Khaitan revealed that the main force was ChatGPT Astra, with some difficult chapters handed to Claude Fable. According to the team's open-source toolkit, at the top on the AI side is the "team leader," that is, the main conversation session with which the researcher directly talks; it does not write proofs, but only guards the mathematical route. Under the leader is a long-running background "scheduler" agent, responsible for splitting work, assigning work, and acceptance checks. The ones actually writing proofs, finding errors, and checking references are a batch of temporary agents that exit after completing one task. The human authors stand at the very top of the whole system, responsible for choosing definitions, setting propositions, and confirming that what is proved in Lean is exactly what mathematicians intended to prove. During the sprint, the team was writing the topology section section by section according to a textbook published in 1977 by topologist Moise. Early on September 20, Claude Fable 5.1, in the role of leader, wrote a work assignment sheet, splitting this section into four parallel task lines and handing them to OpenAI's programming agent Codex. Each task line was allowed to modify only the files under its own name, and after finishing had to return a list, which Claude would accept and then commit. The most important point was: never weaken a proposition just to make it provable. Discovering that a proposition is false also counts as success; if a counterexample is found, stop and report it. By evening, the leader had rearranged a schedule. Estimating based on 3 to 4 parallel task lines, the sections in the book "recognized as the hardest" would take 6 to 10 weeks, and reaching the topological version of Poincare would take at least more than 4 months. Half an hour later, the human lead decided to change the approach: build the skeleton first. That is, first build the structure of the entire proof, temporarily use sorry to hold places for steps that could not yet be proved, so that problems with mismatched interfaces could be exposed in advance, and then review, finalize, and prove the placeholder propositions one by one. These skeleton files were stored separately and not entered into the main repository, so there is still not a single sorry in the final product. On September 23, Ben Chow proved three blocks in Section 32, and the one responsible for acceptance was Claude as leader. After compilation and auditing all reported zero errors, the work submitted by this old professor who had supervised 16 doctoral students was accepted into the main repository. The next day, a string of theorems in the book from 25.2 to 34.1 were all proved. At 3:38 a.m. Eastern Time on September 27, the topological version of Poincare was proved, less than a week after that schedule was laid out.

Suturing together a century of "surgery." Returning to the Poincare conjecture itself. It was proposed by Poincare in 1904, meaning that in a finite, closed three-dimensional space, if any loop of string can shrink to a point, then it is a three-dimensional sphere. This problem dragged on for nearly a hundred years; higher-dimensional versions were conquered early, but the three-dimensional case remained stubborn. It was not until late 2002 to 2003 that Perelman posted three papers in succession on arXiv, using Ricci flow to break the deadlock. The idea of Ricci flow is to iron space out all the way. If a space can be ironed in this way until it is equally round everywhere, then it is a sphere, and the conjecture is proved. The trouble is that space does not necessarily obediently become round. Imagine a dumbbell, with two large balls at the ends and a thin rod connecting them in the middle. Once Ricci flow starts running, the thin rod gets thinner and thinner, and in finite time is pinched off with a snap. At the point of pinching, the degree of curvature tends to infinity, which in mathematics is called a "singularity." Hamilton was stuck at this step for many years. Perelman had the canonical neighborhood theorem, knowing that the place about to go wrong could only be a "neck" or a "cap," so he took out the surgical knife. The method is to cut open from the middle of the neck before the thin tube is pinched off, throw away the small section about to go wrong, and then sew a standard-shaped cap onto each of the two openings, letting Ricci flow continue running. From bottom to top is the direction of time advancement. In his third paper, Perelman also proved that for a simply connected space, if it flows for a while, undergoes surgery once, and then continues flowing, the entire space will shrink to nothing in finite time. Each disappearing piece is a three-dimensional sphere, and gluing them back according to the cut positions still yields a three-dimensional sphere. Many key steps in these three papers only stated conclusions, and it was not until 2006, when several groups of mathematicians successively wrote detailed versions running to hundreds of pages, that the mathematical community confirmed the proof held up. In this repository, the previous 4.02 million lines of code all ultimately serve a file of only 23 lines. The theorem in the file states exactly the Poincare conjecture: any compact, simply connected, boundaryless three-dimensional topological manifold is homeomorphic to the three-dimensional sphere. Ricci flow can only run on smooth spaces, so the Moise theorem is also needed to build a bridge. Moise proved in 1952 that every three-dimensional topological manifold can be cut into small tetrahedra pieced together, and then the seams can be smoothed to obtain a smooth structure. The latter half of those 23 lines of code does exactly "build the bridge first, then cross the river": first use the Moise theorem to obtain a smooth structure, then invoke the smooth version of the Poincare conjecture. The Moise bridge is even more laborious than the surgery part. The PL topology code responsible for it, that is, code that studies space by piecing together small blocks, has 460,000 lines, nearly double the surgery part. Some mathematicians asked in the thread whether the last few lines could simply call the smooth version of Poincare in one line. Khaitan replied that the parameters C and hC cannot be omitted, because Lean must first confirm that this manifold has a set of smooth coordinates. These two parameters are exactly obtained from the Moise theorem.

The end of a Millennium Prize Problem is also the beginning of the next revolution. A year ago, the autoformalization agent Gauss wrote 25,000 lines of code in three weeks, and that was already big news. This time, four people plus a group of AIs wrote more than a hundred times that in two weeks. Stanford mathematician Jared Duker Lichtman, when reposting, typed two exclamation marks in a row. The division of labor of this small team is almost exactly what future mathematical research will look like. Veterans set the direction, young people write code line by line with AI, and whether it is correct is ultimately determined by the Lean kernel. The energy of human mathematicians is shifting from writing proofs step by step to judging what should be proved and ferreting out where AI wrote something wrong. At this pace, the next problem AI helps conquer may be one that no one has proved to this day. 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