China's first model-assisted breakthrough on a world-class maths problem: Intern-S2 and the three-dimensional Ghys conjecture
A rigidity conjecture proposed in 1995
On 15 October Shanghai AI Laboratory announced that the three-dimensional Ghys conjecture, open for more than three decades, had been cracked. A team led by Xu Disheng — a visiting scholar at the laboratory and a professor at Great Bay University — worked with the Intern-S2 science multimodal model in a human-machine collaboration to complete the proof, while teams led by Dong Bin and Liu Ruochuan at Peking University formalised it using their SHEAF framework. The paper is on the arXiv preprint server and the formalisation code is public on GitHub. The laboratory calls it the first time Chinese scientists have used a Chinese model to break a world-class mathematics problem.
What does it claim? Proposed by the French mathematician Étienne Ghys in 1995, the conjecture says that every holomorphic Anosov system on a compact complex manifold is biholomorphically conjugate to a holomorphic affine automorphism of some complex infra-nilmanifold. The laboratory's intuition: imagine a closed, finite "world" with no boundary whose every patch obeys the rules of complex arithmetic. If such a world carries a motion that is at once kneading and perfectly regular, then the world can only be a highly regular shape assembled by repeating simple rules, like a crystal lattice — a complex torus, for instance — and the motion itself is essentially just translation, rotation or scaling within it.
Why is it hard? Xie Junyi of Peking University, an invited 45-minute speaker at the 2026 International Congress of Mathematicians, puts it this way: the difficulty is that the analogous assertion in the real case is still a famously wide-open problem, while the complex case becomes more rigid — an important and very difficult question in the study of rigidity phenomena in complex dynamics. Xu Disheng previously worked on the three-dimensional case with his advisor, Fields Medalist Artur Avila, without arriving at a viable line of proof; he and Zhang Jiesong later obtained partial, weakly related results in three dimensions, published in the Journal of the European Mathematical Society.
It started with an Olympiad AI test
The starting point was how the Intern model performed at the 2025 Chinese Mathematical Olympiad finals. That year the olympiad committee added an AI test for the first time: three Chinese models were invited to sit the same paper as human contestants for the same length of time, marked by the official organisers against the same standard. Intern-S1 scored 102, first among the models taking part and well above the 78-point gold-medal line.
Marking experts found Intern-S1's answers "very close to human expression", and one of its solutions was described as a clever new approach that never appeared in the contestants' scripts. Xu Disheng, whose research spans dynamical systems, spectral theory, fractal geometry and AI for mathematics, noticed the model's potential; having cleared the olympiad bar, Shanghai AI Laboratory was in turn looking to push model capability from competition-level to the harder research level. The two aims converged and in early 2026 they formally began joint model-training research.
The joint team also built a harness system aimed at research mathematics. Drawing on his own research experience, Xu Disheng identified where the model and the system fell short, and real frontier problems drove several rounds of iteration. The resulting Intern-S2 and its supporting system combine large-scale recursive reasoning with highly flexible human-machine interaction, a clear step up in handling complex mathematical propositions.
A thousand pages of derivation, with judgment left to humans
During the effort, Intern-S2 produced a 400-page derivation on its first pass at the three-dimensional Ghys conjecture. From August 2026 it probed the problem from several directions, completing seven successive batches of derivation: the problem graph grew from 15 nodes to 389, total output reached roughly a thousand pages of rigorous derivation, and dozens of entirely new lines of argument emerged, some of them inventive.
The division of labour was clear. The model exploited its strength in long-chain, large-scale derivation — opening parallel branches, decomposing complex propositions and absorbing enormous amounts of laborious work, returning a mass of attempts each round. The researchers steered: judging which lines deserved to be pursued, which were dead ends, and supplying intuitive suggestions as instructions for the next round. The full proof chain was not produced by the model alone; it was assembled through many rounds of dialogue, mutual prompting and trial and error. The paper's author states on arXiv that Intern-S2 was used to help develop mathematical ideas and arguments, but that he independently verified all the mathematics and bears responsibility for it. The paper was completed and written up by Zhang Jiesong, Xu Disheng's student, now at KTH Royal Institute of Technology. Titled "Codimension-one holomorphic Anosov diffeomorphisms", its central theorem proves the codimension-one case of the Ghys conjecture and, in particular, the case of complex dimension three.
One sentence has to be stated precisely: what was solved is the codimension-one case, which includes complex dimension three, and that is not the same as the entire Ghys conjecture being settled. The paper itself discusses obstacles in higher codimension — for instance, the stable and unstable distributions of some higher-dimensional holomorphic Anosov systems may fail to be holomorphic — so the general higher-codimension version cannot be claimed on this basis. Distinguishing "cracking the three-dimensional Ghys conjecture" from "proving the whole Ghys conjecture" is the most accurate way to describe the work.
One telling side note: before the paper went up on arXiv, Xie Junyi received it from the team. Hearing that a Chinese model had been involved, he deliberately tested the problem with GPT-6 and it did not solve it. The laboratory reads this as evidence of Intern-S2's distinctive value in this frontier exploration, and as a signal that Chinese models can compete on the field of advanced mathematics.
Formal verification, and a flywheel
Can AI-assisted results withstand scrutiny? Teams led by Dong Bin and Liu Ruochuan at Peking University formalised all four main theorems of the paper, and the proofs passed Lean's checks. Lean is an interactive theorem prover that subjects formalised proofs to strict logical verification. Jiang Jiedong and Wu Bin, core members of the Peking University team, say the whole process took only about five days, peaked at 100 concurrent agents and produced roughly 550,000 lines of Lean code — an unusually large parallel scale and a very fast verification. Experts confirmed that the formal statements match the semantics of the paper's main theorems.
The difficulty starts with the mathematics: a natural-language proof often assumes the reader will fill in conditions and inferences from background knowledge, whereas formalisation must render all of that into a proof a computer can check. Where a cited result is not already in a foundational library, one has to formalise it too, or find an alternative route using existing results. Formal infrastructure for dynamical systems was thin, and this work added a great deal of it. To organise the effort, the Peking University team used its own SHEAF framework, arranging the paper's propositions, definitions and dependencies into a directed acyclic graph that runs from the target theorem down to foundational libraries, then orchestrating work against that graph while tracking the statement, proof and pruning state of each node.
The boundaries still matter. Lean checks the logical correctness of formalised code: it guarantees that the statements as formalised are rigorously proved, but it cannot automatically guarantee that every natural-language statement, modelling choice and formalised theorem in the paper is faithful. And a paper on arXiv is a preprint, not yet a peer-reviewed publication. Formal verification and peer review are checks of different kinds, and both are needed.
The significance goes beyond one solved problem: the work validates a research pattern. Traditional mathematics depends on long individual exploration by unusually gifted people; this effort wired expert intuition systematically into a machine-solving loop, forming a closed cycle of system exploration, expert judgment, accumulated results and corrective feedback. The laboratory argues the pattern can be replicated in more fields of basic research where the search space is vast and experts are scarce. Next, the team plans to package the capability loop it exercised here into a reusable mathematical verification module on the Intern-Duanyan scientific discovery platform, available for later research problems. Using the three-dimensional Ghys conjecture as a starting point, it also intends to extend the accumulated reasoning ability to disciplines that share mathematical structure, then package any new capability back into the platform — a self-improving flywheel of breakthrough, packaging, reuse and further breakthrough. Whether that promise holds depends on how it performs on the next problem, in some other field.