A research team led by mathematicians from Great Bay University and the Shanghai Artificial Intelligence Laboratory has published a complete proof of the three-dimensional Ghys conjecture, resolving a 31-year-old open problem in dynamical systems. The proof relied on Shanghai AI Lab's Shusheng-S2 multimodal scientific foundation model to explore deduction pathways, followed by formal computer verification in the Lean proof assistant conducted by researchers at Peking University.
The achievement marks the first time a Chinese large language model has contributed directly to proving a major international mathematical conjecture.
The 3D Ghys Conjecture
Formulated by French mathematician Etienne Ghys in his 1995 paper Holomorphic Anosov systems, the Ghys conjecture addresses the geometric classification of complex dynamical systems. The conjecture posits that every holomorphic Anosov diffeomorphism on a compact complex manifold must be biholomorphically conjugate to an affine automorphism of a complex infra-nilmanifold.
In dynamical systems theory, the problem serves as a benchmark for understanding how rigid geometric structures constrain chaotic dynamics. While partial cases and real-variable analogues had been studied over the intervening decades, the three-dimensional complex case remained unproven.
Human-in-the-Loop Reasoning and Proof Synthesis
The informal proof was constructed through an iterative collaboration between domain specialists and Shanghai AI Lab's Shusheng-S2 (internationally designated Intern-S2) reasoning model. Professor Xu Disheng (Great Bay University and visiting scholar at Shanghai AI Lab) and Dr. Jiesong Zhang (postdoctoral researcher at KTH Royal Institute of Technology) structured the exploration using the lab's Harness recursive deduction system.
Beginning in August 2026, the model generated preliminary mathematical derivations across multiple reasoning branches. The human researchers evaluated candidate lemmas and filtered dead ends, guiding the model through seven major deduction cycles. Over the course of the collaboration, the reasoning graph expanded from an initial 15-node outline to 389 validated logical nodes, ultimately connecting all intermediate steps required to close the proof chain.
Machine Verification in Lean
To ensure mathematical validity, an independent verification team at Peking University led by Professor Dong Bin and Chinese Academy of Sciences Academician Liu Ruochuan converted the derivation into formal logic.
Using the Lean proof assistant and Peking University's SHEAF formalization framework, the team orchestrated 100 parallel AI agents over a five-day computational run. The system produced more than 550,000 lines of machine-checked Lean code, formally verifying all four primary theorems without logical gaps. The formalization also establishes foundational software libraries in Lean for complex dynamical systems and holomorphic foliations.
Availability and Methodology
The paper has been released as a preprint on arXiv, and the Peking University verification team has made the complete Lean formalization repository available on GitHub.
While the Lean proof certifies the mathematical correctness of the theorem independently of how it was generated, the underlying Shusheng-S2 model weights and Harness infrastructure remain internal to Shanghai AI Laboratory. The lab announced plans to package the reasoning workflow into a scientific discovery platform dubbed Shusheng-Duanyan for future research applications.
Sources
- HyperAI: Chinese Scientists Use Shusheng-S2 to Prove Ghys Conjecture
- Yicai Global: Chinese Scientists Use Shanghai AI Lab's Scientific Model to Solve First World-Class Math Problem
- TechTimes: Chinese AI Model Helps Prove 31-Year-Old Math Conjecture With Machine-Verified Lean Proof
- CGTN: Chinese Researchers Solve 3D Ghys Conjecture With Homegrown AI Model
