A team led by Xu Disheng, a visiting scholar at Shanghai AI Lab and professor at Greater Bay Area University, has completed a proof of the three-dimensional Ghys conjecture, working with the lab’s Shusheng-S2 scientific multimodal model. The result has been formally verified by a Peking University team, and the paper is on arXiv with the formal code published on GitHub.
The conjecture dates to 1995, when the French mathematician Étienne Ghys proposed that every holomorphic Anosov system on a compact complex manifold is biholomorphically conjugate to a holomorphic affine automorphism of a complex infra-nilmanifold. In plain terms, it asks whether the existence of chaotic dynamical behaviour can determine the geometric classification of the space it happens in. Specialists in dynamical systems regard it as one of the field’s most important long-standing open problems.
What the conjecture actually says
Imagine a closed, finite world with no boundary, where every small patch obeys the rules of complex arithmetic. An Anosov system behaves like kneading dough: pressing, stretching and folding, with some directions stretched and others compressed. The stretching pulls initially adjacent points apart quickly, so a tiny difference in starting conditions produces a completely different trajectory.
Ghys conjectured that if such a motion exists, and is at the same time perfectly regular, then the world can only be a highly regular shape assembled by repeating simple rules, like a crystal lattice. A complex torus is the canonical example.
Seen from the other direction, the motion is then just a simple translation, rotation or scaling of that world. Chaos, in other words, determines geometry.
Xie Junyi, a professor at Peking University’s Beijing International Centre for Mathematical Sciences and a 45-minute speaker at the 2026 International Congress of Mathematicians, described the difficulty: the corresponding assertion in the real case is still a famous open problem, and the complex case is more rigid, making it a central question in the study of rigidity phenomena in complex dynamics.
Xu had worked on the problem for years. He previously studied the three-dimensional case with his doctoral supervisor, the Fields medallist Artur Avila, without arriving at a workable approach, and later obtained partial results with his student Zhang Jiesong that were published in the Journal of the European Mathematical Society.
Seven batches, 389 nodes
Zhou Bowen, director and chief scientist of Shanghai AI Lab, has argued that the older and more fundamental a problem is, the more room AI has to accelerate it, citing monoclonal antibodies, protein folding and the unresolved Navier-Stokes Millennium Prize problem as examples. The three-dimensional Ghys conjecture fits the pattern.
Xu became a visiting scholar at the lab in March 2026, and a joint team was formed with a Harness system built for mathematical research scenarios. Xu used his research experience to identify where the model and system fell short, and real frontier problems drove successive rounds of iteration.
By August the internally iterated Shusheng-S2 had large-scale recursive reasoning and flexible human interaction. On the first round of reasoning against the Ghys conjecture it produced a 400-page derivation report.
The training approach kept to a general-plus-specialist path: large-scale pretraining on scientific knowledge as the base, followed by research-grade post-training data drawn from mathematics papers with reliable verification schemes. On the algorithm side the team worked on asynchronous long-horizon reinforcement learning, addressing exponential error accumulation, long-term state maintenance and self-correction, and built a self-evolution algorithm that distils the gains from the Harness system back into the model.
On benchmarks that stress long, rigorous reasoning, including IMO-Proof and AdvancedMathBench, the company says Shusheng-S2 leads existing open models and exceeds top closed models such as Gemini 3.1 Pro on some measures.
Human in the loop, by design
The division of labour was explicit. Shusheng-S2 ran many branches in parallel, decomposed the problem, generated competing strategies and carried the volume of derivation, returning large numbers of attempts each round. Xu and Zhang supplied direction: which lines deserved depth, which were dead ends, and where intuition suggested a different framing.
Neither side derived alone. The work moved through repeated dialogue and feedback. On the model’s first-round exploration, the mathematicians identified the key opening and kept calibrating the direction. Across the project the system completed seven successive batches of derivation, the problem graph grew from 15 nodes to 389, and the output reached more than a thousand pages of rigorous derivation while generating dozens of new argumentative strategies.
One detail is worth noting. Before the paper went to arXiv, Xie Junyi had tried the same problem with GPT-6 and did not find a proof.
The verification is the part that matters
Whether AI-assisted mathematics can be trusted depends entirely on the checking. The teams of Dong Bin and Liu Ruochuan at Peking University formalised all four main theorems and verified them in Lean, the interactive theorem prover that mechanically checks formal proofs for logical correctness.
The process took about five days, peaked at 100 concurrent agents and produced roughly 550,000 lines of Lean code. Experts confirmed that the formal statements match the semantics of the paper’s main theorems, so the Lean verification establishes strict correctness.
The difficulty is partly mathematical and partly infrastructural. Natural-language proofs rely on the reader to supply conditions and inferences, while formalisation has to make every step machine-checkable. Cited results missing from the standard library require either new formal proofs or alternative routes through existing results. Dynamical systems had thin formal infrastructure, so the team added a large amount of it to cover the literature the paper depends on.
To organise that, the Peking University team used its own SHEAF framework, in which multiple agents arrange the propositions, definitions and dependencies into a directed acyclic graph running from the target theorem down to the foundational library. The agents then work on decomposition and formal proof construction under that graph, tracking statement, proof and pruning status at each node.
From one theorem to a research pipeline
The Peking University group has been working on AI for mathematics since 2021, before large models were usable, and has built tooling across evaluation sets, large-scale mathematical retrieval, automated reasoning and formal verification. Its systems have previously resolved the Anderson conjecture, the first time a university-led team independently cracked a major open mathematical conjecture with AI, and the group has separately completed a formal verification of the Poincare conjecture.
The broader significance here is methodological. Traditional mathematics depends on individual talent and long solitary effort. This project wired expert intuition into a machine search loop, producing a cycle of systematic exploration, expert judgement, accumulated results and corrective feedback. That cycle is transferable to other fields with enormous search spaces and scarce specialists.
Shanghai AI Lab intends to package the verification capability as a reusable mathematics module in its Shusheng Duan Yan science discovery platform, then extend the reasoning capability to disciplines with related mathematical structures, packaging each new capability back into the platform for the next round.
Editor’s note: This is an adapted translation of the original Leiphone report. It has been trimmed and restructured for readability for an international business audience. The full original (in Chinese) is at https://www.leiphone.com/category/academic/ChIK9FvwSwlHmfFc.html.