AI for Mathematics · 2026
Human–AI Collaboration on the Ghys Conjecture
Helping mathematicians solve the three-dimensional Ghys conjecture through human–AI collaboration: Intern-S2 combines large-scale recursive reasoning with expert insight to tackle a problem open for more than 30 years.
From competition mathematics to mathematical discovery
My work on mathematical reasoning at Shanghai AI Laboratory contributes to a broader goal: making AI a useful research partner for mathematicians. In this project, Disheng Xu and Jiesong Zhang worked with Intern-S2 and its research harness to prove the three-dimensional Ghys conjecture. A separate Peking University team led by Bin Dong and Ruochuan Liu carried out formal verification using the SHEAF framework.
Proposed by Étienne Ghys in 1995, the conjecture asks whether holomorphic Anosov dynamics on a compact complex manifold force a rigid algebraic structure. The three-dimensional case connects complex geometry and dynamical systems: seemingly chaotic motion can impose surprisingly strong constraints on the space supporting it.
A research process shaped by human insight
The collaboration paired the model’s ability to explore many lines of reasoning with the mathematicians’ judgment about which ideas were promising. The early exploration was particularly important: an initial report of roughly 400 pages exposed potential routes, including ideas from neighboring areas of mathematics. Experts identified useful insights, rejected dead ends, and guided subsequent exploration.
Across seven rounds of continued reasoning, the problem graph expanded from 15 to 389 nodes, producing over a thousand pages of derivations. The system decomposed difficult questions, explored alternative arguments, and accumulated intermediate results; the researchers continually refined the direction and assembled the final proof.
Verification and a reusable research workflow
According to the laboratory’s report, the Peking University team formalized all four main theorems of the resulting paper, Codimension-one holomorphic Anosov diffeomorphisms, with proofs checked in Lean. This verification complemented the mathematical discovery process.
The project demonstrates a workflow in which systematic exploration, expert judgment, accumulated results, and feedback reinforce one another. In my interview with Yicai, I emphasized that AI increases the amount of intellectual work researchers can carry out, while humans remain responsible for research direction and value.
Read more
- Shanghai AI Laboratory: 中国科学家首次用中国大模型攻克世界级数学难题 · October 15, 2026 (Chinese)
- Yicai: 国产大模型攻克世界级数学难题 · October 17, 2026 (Chinese)
- Public formalization code: HolomorphicAnosov