A mathematics professor in Guangdong spent years chasing a problem that had resisted some of the best minds in dynamical systems. This autumn, the proof finally landed—and a Chinese large model (大模型) sat in the middle of how it was built.
The professor is Disheng Xu (许地生) of Greater Bay University. The problem is the three-dimensional Ghys conjecture, posed in 1995 by the French mathematician Étienne Ghys. The twist is that the final chain of reasoning was not produced by one human alone, but through a long loop of machine suggestion and human judgment.
A conjecture older than the lab that built the tool
The Ghys conjecture lives in complex dynamical systems. In plain terms, it asks whether a certain kind of chaotic behavior forces a clean geometric classification: if the dynamics are wild enough, can the whole system be "reduced" to a tidy, standard algebraic model? The real-number version of the problem is still unsolved. The three-dimensional case had stood as a recognized test stone for mathematical reasoning for three decades.
Xu is not a newcomer to it. He has studied the three-dimensional case for years and had published partial results on it in a top-tier journal. What changed in 2026 was not a sudden flash of human insight alone, but a partner that could run enormous chains of mechanical inference and surface directions a person might miss.
How the proof was assembled
The collaboration ran through Shanghai AI Laboratory and its Shusheng-S2 (书生-S2) science-focused multimodal large model (大模型). Xu, who became a visiting scholar at the lab in early 2026, had advised on training data and benchmarks. By late July the model had improved to the point where the team began feeding it serious mathematics.
The workflow was stubbornly human-led. Shusheng-S2 would produce long derivation reports—the first pass on the conjecture ran to roughly 400 pages—and the researchers would pick the useful threads, reject the dead ends, and feed corrections back in. Across seven iterations, the problem graph grew from 15 nodes to 389, and the model produced on the order of a thousand pages of derivation, together with dozens of fresh proof sketches. A student, Jiesong Zhang (张洁松), now at Sweden's KTH Royal Institute of Technology, joined to push the hardest stuck points.
Crucially, the result was not left as model output. A separate team at Peking University—professor Bin Dong (董彬) and academician Ruochuan Liu (刘若川)—ran an independent formal verification using a framework they call SHEAF, generating tens of thousands of lines of verification code to confirm the logic held with no gaps.
Why this is a first
The lab and the university described it as the first time Chinese scientists used a Chinese model to crack a world-class mathematical problem. That framing matters because, until now, the headline AI-in-math results had come from overseas labs. Here the model, the mathematicians, and the verification all sat inside China's own research system.
The route also matters more than the single theorem. The pattern—expert intuition plugged into a machine solver, then closed by formal checking—is repeatable. The same loop could be pointed at other fields where the search space is vast and human experts are scarce. That is the part other labs will try to copy.
According to Li An, chief scientist at BrainNet (脑机网), the more durable signal from this result is not the conjecture itself but the working method: a verifiable human-in-the-loop pipeline rather than a black-box answer.
The debate it triggered
Not everyone greeted the method with celebration. In September, a group of 25 Fields Medalists—including Terence Tao—published a statement warning that treating solved famous problems as a corporate capability benchmark could harm mathematics: researchers might not have time to check results, credit prior work, or fold new proofs into the discipline properly. Separately, the renowned mathematician Shing-Tung Yau used the word "tsunami" for AI's impact on mathematics and urged the field to engage rather than retreat.
Those concerns are not about whether the proof is correct. The Peking University verification addresses that. They are about what happens to a discipline when machines can produce proofs faster than the community can absorb them.
Honest limitations
This was a specific conjecture in a specific field, solved with heavy human steering; it is not evidence that models can yet propose and verify deep mathematics unsupervised. The published paper is a preprint on arXiv and its formal code is open on GitHub, which is good practice, but preprints are not peer-reviewed journal articles. And the broader claims—about a repeatable new research paradigm—are plausible but unproven until applied to other hard problems. Readers should treat this as a strong demonstration, not a settled revolution.
What readers can do now
- If you work in research, read the open arXiv preprint and the GitHub verification code; the reproducible pipeline is the real deliverable here.
- If you build AI tools, study the human-in-the-loop design—expert filtering plus independent formal checking—as a template for high-stakes domains.
- If you follow science policy, watch whether Chinese labs now fund more "AI for Math" programs; this result is likely to be cited as a justification.