A Chinese AI Model Helped Crack a 30-Year-Old Math Conjecture
Shanghai Artificial Intelligence Laboratory says its scientific multimodal model Shusheng-S2 helped prove the three-dimensional Ghys conjecture, open for more than three decades — then handed the result to Peking University mathematicians, who verified it with a formal proof-checking framework.
The Shanghai Artificial Intelligence Laboratory announced on October 15 that a team working with its scientific multimodal model, Shusheng-S2, had produced a proof of the three-dimensional Ghys conjecture — a problem posed by the French mathematician Étienne Ghys that has resisted mathematicians for more than thirty years. The lab billed it as the first time Chinese scientists have used a homegrown large model to crack a world-class open problem.
The claim's architecture matters more than its patriotism. A team led by Xu Disheng, a visiting scholar at the lab and professor at the Greater Bay Area University, paired the model with human collaborators along what the lab calls a "generalist-plus-specialist fusion" route: the model grinding through the search space, humans steering and judging. The result then left the lab that produced it. A Peking University team around Professor Dong Bin and the academician Liu Ruochuan ran the proof through SHEAF, a framework for formal verification, and confirmed the argument is correct. In other words, the machine's work was certified by a checker that does not take anyone's word, machine or human.
That division of labor is precisely what the week's louder AI-math fight has been missing. Ten days ago, top mathematicians led by Terence Tao called for a boycott of OpenAI's machine-generated proofs as we covered at the time, objecting to unverifiable AI claims entering a field whose currency is certainty. The Ghys announcement is, deliberately or not, an argument for the other reconciliation: the model proposes, the formal checker disposes, and no one is asked to trust the machine's prose.
On Zhihu, where the news reached the fifth slot of the day's hot list, the discussion dwelt on exactly that boundary — what "human-machine collaboration" means when the collaboration can be audited but the labor cannot, and whether a proof with a model inside it changes what authorship is. The skeptics wanted to know how much of the genuinely hard work the model did; the partisans noted that thirty years of humans alone had not closed it. Both camps, notably, accepted the result itself, because the SHEAF verification left nothing to take on faith.
The conjecture itself, a statement in three-dimensional dynamical systems, will now face the normal siege of peer review — the lab's formal verification does not exempt it from that. But the template is the news: a Chinese lab has put an LLM inside a proof pipeline at the moment its field is deciding whether such proofs deserve to exist, and the pipeline's answer is to make the machine show its work.