An AI Helped Prove a Thirty-Year-Old Conjecture, and Lean Checked Every Step

A thirty-year-old conjecture, a Chinese model, and a machine-checked proof

On October 15, Shanghai AI Laboratory announced that a research team had proven the three-dimensional case of the Ghys conjecture, an open problem in dynamical systems that has stood since 1995. The work was developed with the laboratory's own Intern-S2 model, and the finished proof was formally verified in Lean by a team at Peking University.

The relevance is not only that a hard problem fell. It is that the announcement was structured around process rather than around a number: a model producing derivations, researchers choosing which lines of attack to fund with attention, and a proof assistant certifying every step. That combination is what the industry has been promising for two years, and here it is with a paper attached.

What the conjecture asks

Étienne Ghys proposed the problem in 1995. In broad terms it asks whether the behavior of chaotic dynamical systems can determine their geometric classification, which is a way of asking whether motion tells you the shape of the space it happens in.

The general question is not what got solved. The team proved the codimension-one case, which is the three-dimensional setting, and which had remained open for three decades. That distinction matters for reading the claim honestly: the full conjecture remains broader, but the specific case that had resisted everyone until now is now settled.

The first pass produced four hundred pages

The mechanics of the collaboration are more interesting than the result, because they show what human-AI research actually looks like minute to minute.

Intern-S2's first exploration of the problem produced a derivation report of roughly 400 pages. That is not an answer. It is a pile of candidate reasoning, some of it useful and some of it not, which is precisely the shape of output you get when a model is asked to think through something genuinely unsolved rather than to recall something known.

From there, the work ran through seven rounds of continued reasoning. The problem graph, a map of sub-claims and how they depend on each other, grew from 15 nodes to 389. The accumulated output reached about a thousand pages and included dozens of distinct approaches. At each stage, the mathematicians did the thing the model cannot do for itself: they looked at the proposals, decided which openings were promising, and steered the next round.

Xu Disheng, a visiting scholar at the laboratory and a professor at Greater Bay University, and Zhang Jiesong, a postdoctoral researcher who had tracked the conjecture since his doctoral studies, supplied that judgment. Zhang's paper, posted to arXiv on September 29 and revised on October 13, is a single-author work with a declaration of AI use: the model helped develop the ideas and arguments through multiple rounds of dialogue, and he independently checked the mathematics.

The part that makes it more than a story

Claims about AI solving mathematics are cheap. What gives this one weight is that the proof was formalized.

Peking University's team, led by Bin Dong and Ruochuan Liu, used its own SHEAF framework to formalize all four main theorems, plus the supporting results by Ghys that the arguments depend on. Formalization means translating the definitions, assumptions, and reasoning into a language a computer can check, where every step of the writer's argument has to be spelled out instead of being left for a trained reader to fill in.

The effort took about five days, with as many as 100 agents working in parallel, and produced roughly 550,000 lines of Lean code. Lean is an interactive theorem prover. It does not care how confident anyone feels. It checks the logic, and it either accepts the proof or it does not.

SHEAF organized the task as a directed graph of definitions, propositions, and dependencies, so that separate agents could work on connected pieces while the team tracked which statements had proofs and which still needed them. That is a genuinely new kind of labor division, and the framework also had to patch gaps in the existing formal library for dynamical systems, because the machinery this proof needed simply was not there yet.

Human and model, doing different jobs

The division of labor described by the lab is worth taking at face value, because it is not the flattering version for either party.

The model combed literature, broke the proposition into pieces, explored proof branches in parallel, checked logical steps, and tested a large number of ideas fast. The humans set direction, judged which approaches were worth pursuing, and made the calls that decided where to spend the next round of effort.

Neither half resembles the other. The model's contribution is scale and stamina: it can hold dozens of dead ends in mind without getting discouraged. The humans' contribution is taste, which is the ability to look at a hundred pages of plausible reasoning and know which three paragraphs matter.

There is an anecdote attached that the Chinese press made a great deal of. A dynamical systems expert reportedly ran the same problem past GPT-6 out of curiosity after hearing a domestic model had solved it, and it did not get there. Read narrowly, that is a comparison between two systems on one problem, which proves very little. Read as a signal about competitive dynamics, it is the kind of detail that drives investment.

Why formal verification changes the stakes

For most of the last two years, the bottleneck in AI-assisted mathematics has not been generating candidate arguments. Models are good at producing plausible reasoning. The bottleneck has been knowing which of it is correct, because checking a proof is slow, expert, and does not parallelize well.

Lean inverts that. Once a statement is formalized, verification is cheap and fast, and it can be trusted because it is mechanical rather than social. The 550,000 lines are the expensive part, and the fact that a team plus a hundred agents could produce them in five days is the real advance here. It suggests that the verification bottleneck may be loosening just as the generation bottleneck was already loose.

The lab says it will package the workflow as a reusable mathematical verification module on its scientific discovery platform, connecting the model, agents, data, and experimental equipment. It also cites an earlier result, in which a team at Wuhan University used the platform to cut the development cycle for an electrochemical synthesis from five to ten years down to one to two.

What to take from it

The honest summary is that this is a real result with a real proof, produced by a workflow that is still very human-intensive. Seven rounds of expert steering is not a model running on its own. A single-author paper with a declaration of AI use is not a model claiming credit.

What has changed is that the loop now closes. A model can produce enough reasoning to matter on a problem nobody has solved, humans can direct it, and a proof assistant can certify the outcome without anyone having to trust a summary. That is a pipeline, not a demo, and pipelines are what turn a capability into a practice.

The next question is whether this generalizes past the cases where formalization is even possible. Geometry and dynamics have some structure that lends itself to machine checking. Much of the rest of science does not, and it is in that messier territory, in biology, materials, and medicine, that the promise of AI as a research assistant will actually be tested. The Ghys result says the tool can work. It does not yet say how often.