Mathematicians and Shanghai AI Lab's Intern-S2 resolve Ghys's conjecture in complex dimension three
来源：上海人工智能实验室｜2026.10.15
Abstract
The result emerged from a sustained collaboration involving Disheng Xu, a professor at Great Bay University and visiting scholar at Shanghai AI Lab, and his student and collaborator Jiesong Zhang of KTH Royal Institute of Technology. Zhang’s paper establishes the codimension-one case of the conjecture, which includes complex dimension three.
All four main theorems have been formalised and checked in Lean by the team of Prof. Bin Dong and Prof. Ruochuan Liu at Peking University, using their SHEAF framework. Experts also checked that the formal statements matched the mathematical claims in the paper. The preprint and formalisation codes are publicly available.
The result marks an important step for AI-assisted mathematical research: a longstanding open problem has been resolved through repeated interaction between mathematicians and a reasoning model, followed by formal verification of the main results.
What makes the problem difficult
In 1995, French mathematician Étienne Ghys proposed a classification of holomorphic Anosov systems. These systems combine two demanding conditions: their evolution respects the complex structure of the underlying space, while stretching in some directions and contracting in others.
The stretching can cause nearby trajectories to separate rapidly, producing chaotic behaviour. Yet the conjecture predicts that the existence of such dynamics places strong restrictions on the geometry of the space itself. Beneath the complicated trajectories, there should be a precise algebraic structure.
The new paper proves that, in the codimension-one setting, the space must be a complex torus and the dynamics can be transformed, through a holomorphic change of coordinates, into a hyperbolic torus automorphism. This settles the conjecture in complex dimension three. The conjecture remains open in higher dimensions in general.
Disheng Xu had studied the three-dimensional case with his doctoral adviser, Fields Medallist Artur Avila, without finding a successful proof strategy. Later work with Jiesong Zhang produced related results published in the Journal of the European Mathematical Society. The problem remained a continuing focus of their research.
From competition mathematics to an open research problem
The collaboration began with a different test of mathematical reasoning. In the 2025 Chinese Mathematical Olympiad finals, Intern-S1 scored 102 points in an official AI evaluation, above the human gold-medal threshold of 78. Models were given the same time allowance and graded against the same standards as human contestants.
For Xu and the Shanghai AI Lab team, this raised a harder question: could the reasoning behind strong competition performance be developed into a useful capability for research mathematics, where neither the route to a proof nor the answer is known?
Joint research began in early 2026. The team developed a system around the model to support extended mathematical exploration, with Xu using frontier research questions to identify weaknesses and guide successive improvements.
Shanghai AI Lab’s Intern-S2 combines broad scientific pretraining with specialised training on research mathematics. The team also developed reinforcement learning methods for long reasoning sequences and methods for training the model on successful reasoning produced with the surrounding system. Together, these efforts supported longer investigations and more flexible interaction with researchers.
How mathematicians and the model worked together
Beginning in August 2026, Intern-S2 and its supporting system explored Ghys’s conjecture from multiple directions. Its first round produced a roughly 400-page report of candidate arguments and derivations.
Xu and Zhang identified a promising opening in that material. They then used repeated dialogue to test the reasoning, redirect unproductive approaches and develop the most useful ideas further.
Across seven successive rounds of exploration, the system’s problem graph expanded from 15 to 389 nodes. It generated around a thousand pages of working material and dozens of possible lines of argument. These outputs were intermediate research material that the mathematicians had to assess, refine and connect into a proof.
The model could pursue long calculations and explore multiple branches of a problem. The mathematicians brought knowledge of the field, recognised which ideas might matter and judged whether an argument could survive closer scrutiny. Their feedback shaped the next round of exploration.
The eventual proof grew out of that interaction. In the paper’s declaration of AI use, Zhang states that he used an internal version of Intern-S2 to help develop the mathematical ideas and arguments through multiple rounds of dialogue. He independently verified the arguments and takes full responsibility for the manuscript.
From a mathematical argument to a checked proof
A new proof must withstand detailed scrutiny. The Peking University team addressed this by translating the paper’s four main theorems into Lean, a proof assistant that checks formal mathematical reasoning.
The work was carried out by Jiedong Jiang and Bin Wu using SHEAF, the team’s framework for organising large formalisation tasks. The team reports that the process took about five days, involved up to 100 agents working concurrently and produced approximately 550,000 lines of Lean code.
The challenge extended beyond translating the paper sentence by sentence. Informal proofs rely on background knowledge and intermediate steps that a mathematical reader supplies. Formalisation requires these dependencies to be made explicit. Where relevant results were missing from the available libraries, the team had to build additional foundations or find alternative routes using existing formal results.
SHEAF organised definitions, statements and proof dependencies into a directed acyclic graph, allowing interconnected tasks to be developed and checked in parallel. Experts checked that the final formal statements expressed the theorems in the paper, while Lean checked the formal proofs under their stated assumptions.
The repository documents one remaining external mathematical input: a classical theorem on the rigidity of homotopy tori, proved by Hsiang and Wall in 1969, is supplied as an explicit hypothesis for three of the four formalised theorems. The fourth does not require it.
What this means for scientific research
This work demonstrates a practical way to connect AI reasoning with specialist expertise. Researchers selected a meaningful open problem, used the model to broaden the exploration of possible arguments and applied their judgment throughout. Formalisation then provided a separate, machine-checkable test of the resulting reasoning.
That combination matters for fields where the space of possible approaches is large and expert attention is scarce. The result gives us a concrete basis for exploring how similar workflows might help researchers pursue other difficult questions.
Our next step is to turn the capabilities developed through this collaboration into a reusable mathematics verification module within Shanghai AI Lab’s scientific discovery platform. We also plan to investigate how the reasoning methods can support problems with related mathematical structures in other disciplines.
The goal is to make rigorous exploration easier to build on, so that progress on one problem can equip researchers to tackle the next.
Read the research
Paper: Codimension-one holomorphic Anosov diffeomorphisms
https://arxiv.org/abs/2609.37695
Formalisation code
https://github.com/frenzymath/HolomorphicAnosov
SHEAF framework
https://github.com/frenzymath/SHEAF
Contact
For questions about the research or academic collaboration, please contact xudisheng@gbu.edu.cn , zhangjiesong-xuezhe@shlab.org.cn.
For media enquiries, interview requests or communications materials, please contact: comm@pjlab.org.cn.