A team led by Xu Disheng, a visiting scholar at Shanghai Artificial Intelligence Laboratory (Shanghai AI Laboratory) and professor at the Greater Bay Area University, relying on the Intern Scientific Multimodal Large Model S2 (Intern-S2) and following the "general-specialist fusion" technical path, completed the proof of the three-dimensional Ghys Conjecture through human-machine collaboration. A team led by Professor Dong Bin and Academician Liu Ruochuan of Peking University used their self-developed SHEAF framework to complete the formal verification of the proof, confirming the correctness of this work. Industry insiders believe this marks the first time Chinese scientists have conquered a world-class mathematical problem using a Chinese large model.
The "Ghys Conjecture" was proposed by the French mathematician Étienne Ghys in 1995, conjecturing that every holomorphic Anosov system on a compact complex manifold is biholomorphically conjugate to a holomorphic affine automorphism on some complex infra-nilmanifold. The problem combines theoretical difficulty with landmark disciplinary value, and is recognized by mathematical experts in the field of dynamical systems as one of the most important long-standing open problems in the field, a touchstone for testing mathematical reasoning ability.
The related paper has been released on the preprint platform (arXiv), and its formalization code has also been made public on Github.
The Ghys Conjecture: Finding the "Underlying Code" for Chaotic Systems
In 1995, the French mathematician Étienne Ghys proposed the Ghys Conjecture, whose core question is: whether the existence of chaotic dynamical system behavior can determine the geometric classification.
This is an important problem in the field of complex dynamical systems. If the conjecture holds, the problem of chaotic dynamical trajectories can be "reduced" to concise, well-ordered standard algebraic models.
How can the Ghys Conjecture be understood? Imagine a "world" that is closed and finite, without boundary, where every small piece follows the rules of complex number arithmetic.
For Anosov systems, a kneading-dough analogy can help: pressing, stretching, and folding dough, with some directions being stretched and others compressed. The stretching effect makes initially adjacent points separate rapidly—tiny differences in initial conditions lead to completely different evolutionary outcomes.
The Ghys Conjecture says that as long as such a "dough-kneading yet perfectly regular" motion exists, then this "world" can only be a shape formed by repeatedly piecing together simple rules, highly regular like a crystal lattice. For example, a complex torus:
From another perspective, this motion is essentially a simple translation, rotation, or scaling of this "world." In other words, the motion is too chaotic, which in turn determines what shape the world can only grow into. Professor Xie Junyi of Peking University's Beijing International Center for Mathematical Research, an invited 45-minute speaker at the 2026 International Congress of Mathematicians, commented: "The difficulty of the Ghys Conjecture lies in the fact that the analogous assertion for its real (number) version remains a famous, completely open problem; the complex case makes the problem more rigid, and it is an important problem in the study of rigidity phenomena in complex dynamical systems—very difficult."
Professor Xu Disheng of the Greater Bay Area University has long been deeply engaged in research on this conjecture. He previously collaborated with his advisor, Fields Medalist Professor Artur Avila, on the three-dimensional case, but did not form an effective proof strategy; afterwards, he collaborated with his student Dr. Zhang Jiesong to obtain partial weakly related results on the Ghys Conjecture in the three-dimensional case, with the related results published in the top mathematics journal "Journal of the European Mathematical Society" (JEMS).
7 successive batches of deduction and 389 nodes: human-machine collaboration achieves a key breakthrough
"Scientific discovery is the ultimate test of intelligence." Zhou Bowen, Director and Chief Scientist of Shanghai Artificial Intelligence Laboratory, once made a judgment: the older and more fundamental a problem is, the greater the room for AI to improve efficiency—monoclonal antibodies, protein folding, and the still-unsolved Millennium Prize Problem, the Navier-Stokes equations, all conform to this rule. The three-dimensional Ghys Conjecture is precisely one such fundamental difficult problem.
In March 2026, Professor Xu Disheng became a visiting scholar at Shanghai AI Laboratory, and his research collaboration with Shanghai AI Laboratory thus entered a deeper, closer stage. The two sides formed a joint team and simultaneously built a Harness system oriented toward mathematical research scenarios. Drawing on his mathematical research experience, Professor Xu precisely identified the capability shortcomings of the model and the system; relying on real frontier mathematical research problems, he drove the system through multiple rounds of iterative refinement.
In August, the internally iterated Intern-S2 and its accompanying system possessed large-scale recursive reasoning capabilities along with highly flexible human-machine interaction capabilities, achieving a qualitative leap in handling complex mathematical problems. Notably, in its first round of reasoning on the three-dimensional Ghys Conjecture, Intern-S2 produced a 400-page derivation report.
At the training strategy level, the research team adhered to the "general-specialist fusion" technical route. On the foundation of large-scale scientific knowledge pretraining to solidify the model's base, they carefully constructed research-grade post-training data, including large numbers of difficult problems from mathematical papers and reliable verification schemes, enhancing the model's professionalism, rigor, and standardization in research-level mathematics.
At the training algorithm level, the research team broke through asynchronous long-horizon reasoning reinforcement learning training methods, solving a series of fundamental problems under verifiable rewards, including exponential error accumulation, long-term state maintenance, and self-correction. The team also developed a self-evolution algorithm that reverse-distills the capability gains brought by the Harness back into the model, continuously obtaining effective supervision signals on a large number of highly difficult problems beyond the model's direct inference capability boundary, advancing the model's autonomous capability improvement.
On benchmarks emphasizing long-horizon rigorous reasoning, such as the competition mathematics and advanced mathematics benchmarks IMO-Proof and AdvancedMathBench, Intern-S2 leads existing open-source models overall, and surpasses top closed-source models such as Gemini 3.1 Pro on some metrics, ranking among the world's strongest open-source models in long-horizon reasoning capability.
At this point, the base capabilities of Intern-S2 had reached the basic level needed to assist research teams in tackling research-level mathematical problems, but truly cracking a world-class problem required going one step further. The team believed the key to the breakthrough lay in closer human-machine collaboration:
Intern-S2 and its accompanying system leveraged their strengths in long-chain large-scale deduction, spreading out multiple parallel branches, attempting, decomposing complex problems, and hypothesizing different approaches, taking on massive tedious derivation work and delivering enormous amounts of attempt results in each iteration; the researchers were responsible for grasping the overall direction, judging which approaches were worth digging into, which paths were dead ends, and offering intuitive suggestions as instructions for the system's next round of iteration. The two sides did not deduce independently, but rather collaborated through multiple rounds of dialogue and feedback, iterating in close interaction.
The figure shows the system's multi-round interaction process and the recursive solving structure in each round of interaction. Here, edges only represent decomposition relationships between subproblems, not contextual dependency relationships; every node can access all global context that precedes it temporally.
Building on the first round of exploration provided by the AI, the mathematicians Xu Disheng and Zhang Jiesong keenly seized the key breakthrough point, continuously providing feedback to the model and calibrating the exploration direction, guiding the model to dig deep into promising ideas. During the research effort, Intern-S2 successively completed 7 successive batches of deduction, with the problem graph expanding from 15 nodes to 389, outputting a total of over a thousand pages of rigorous derivation while generating dozens of entirely new lines of argument, successfully helping the team crack this world-class mathematical problem, earning the evaluation from international leading scholars in this field of "a depth of thinking far beyond expectations."
Interestingly, before the paper was uploaded to the preprint site arXiv, the aforementioned dynamical systems expert Professor Xie Junyi had also attempted this problem using GPT-6 and did not find a proof. "This not only confirms the unique value of Intern-S2 in this frontier mathematical exploration, but also sends a signal—Chinese large models are equally capable of stepping onto the frontier mathematics arena and helping tackle world-class problems."
The Peking University Team Provides Professional Formal Verification
Can the AI-assisted results withstand verification?
A team led by Professor Dong Bin and Academician Liu Ruochuan of Peking University completed the formal verification of all four main theorems of this paper, with the proof passing the Lean check. Lean, as an interactive theorem proving system, can perform rigorous logical checks on formalized proofs. Jiang Jiedong and Wu Bin, core members of the Peking University team, explained that the entire process took only about 5 days, with peak concurrency reaching 100 agents, producing approximately 550,000 lines of Lean code, demonstrating enormous parallel scale and extremely fast verification speed. Experts confirmed that the formalized statements are semantically consistent with the paper's main theorems, and the Lean verification thereby ensures their rigorous correctness.
The difficulty of formalization comes first from mathematics itself: natural language proofs often rely on the reader's mathematical knowledge to complete conditions and reasoning, whereas formalization must translate them into a complete proof that a computer can check. If results cited in the paper are not already in the foundational theorem library, formalized proofs must be supplemented, or alternative routes using existing results must be found. In particular, the field of dynamical systems originally lacked sufficient formalization infrastructure, and this work supplemented a large amount of infrastructure, covering the numerous literature results the paper depends on. For research-level mathematics, this work involves the accurate expression of definitions, the decomposition of proof structures, and the selection of mathematical tools; when a large number of agents run in parallel, it is also necessary to ensure that the definitions, statements, and dependencies of each part are properly connected, so that local proofs can form a complete proof chain.
To organize this process, the Peking University team used their self-developed SHEAF framework: multiple agents organized the propositions, definitions, and dependency relationships in the paper into a directed acyclic graph extending layer by layer from the target theorem to the foundational theorem library; the model participated in proposition decomposition and formal proof construction within the framework, and the team orchestrated work around this graph, tracking the statement, proof, and pruning status of each node, decomposing the large-scale formalization task into interconnected, checkable steps.
As early as 2021, before large models had even emerged, the team of Professor Dong Bin at Peking University's Beijing International Center for Mathematical Research had keenly perceived that artificial intelligence would reshape the paradigm of mathematical research. The Peking University mathematics team is one of the earliest research teams internationally to lay out the AI for Math direction, building a complete technical chain covering high-difficulty evaluation sets (FATE), large-scale mathematical knowledge retrieval (Matlas/LeanSearch), and automated reasoning and formal verification (Rethlas/Archon/Danus/Iteris); their developed AI system successfully solved the open mathematical problem known as the Andrews Conjecture, achieving the first case in China—and the first internationally—of a university-led team using artificial intelligence to autonomously break through a major mathematical conjecture. Recently, the team also independently completed the formal verification of the Poincaré Conjecture.
From Solving a Single Hard Problem to Research Infrastructure
The significance of this research also lies in validating a new research paradigm. Traditional mathematical research has relied on the long exploration of individual geniuses, whereas this breakthrough systematically integrated expert intuition into the machine solving loop, forming a closed loop of "systematic exploration—expert judgment—accumulation of results—feedback correction." This paradigm can be replicated and extended to more fundamental research fields characterized by "vast search spaces and scarce experts," achieving more "from 0 to 1" original innovative breakthroughs.
Next, building on the complete capability loop validated by this research, the team will further package it into a reusable mathematical verification module of the InternBootcamp scientific discovery platform (书生·端砚), which can be directly invoked for subsequent scientific problem research. Meanwhile, taking the breakthrough on the 3D Ghys conjecture as a starting point, Shanghai AI Laboratory will extend its accumulated reasoning capabilities to other disciplines homologous to mathematical structures; after achieving new breakthroughs, the new reasoning capabilities will be packaged back into the 端砚 (Bootcamp) platform for reuse and combined with more disciplines in pursuit of the next round of breakthroughs, forming a self-evolving flywheel of "breakthrough—packaging—reuse—new breakthrough." Leiphone (WeChat account: 雷峰网) will continue to follow the latest developments in this direction.
This is an original article by Leiphone. Unauthorized reproduction is prohibited. For details, seeReprint Notice。