IT之家 · 智能时代 · 10/15/2026, 11:23:31
Shanghai AI Lab Solves 3D Ghys Conjecture Using S2 Model with Formal Verification
A team from Shanghai AI Lab solved the 30-year-old 3D Ghys conjecture using the S2 multimodal scientific model via a human-AI collaborative approach. The proof was formally verified by Peking University's SHEAF framework, confirming its correctness. This breakthrough validates a new research paradigm integrating expert intuition into machine reasoning loops, with papers and code now publicly available.
SOURCE COVERAGEFull Original Report
On October 15, the Shanghai AI Laboratory announced that a world-class mathematical problem that had puzzled the field for over three decades—the three-dimensional Ghys conjecture—has been solved.
The team led by Xu Disheng, a visiting scholar at the Shanghai AI Laboratory and professor at the Greater Bay Area University, leveraged the Intern-S2 scientific multimodal large model (Shusheng-S2) and adopted a "general-specialized fusion" technical approach to complete the proof of the three-dimensional Ghys conjecture through human-AI collaboration.
Professor Dong Bin and Academician Liu Ruochuan’s team from Peking University used their SHEAF framework to perform formal verification of this proof, confirming its correctness. This marks the first time Chinese scientists have used a domestic large model to conquer a world-class mathematical challenge.
Proposed by French mathematician Étienne Ghys in 1995, the Ghys conjecture posits that every holomorphic Anosov system on a compact complex manifold is biholomorphically conjugate to a holomorphic affine automorphism on some complex infra-nilmanifold. The problem combines theoretical difficulty with disciplinary landmark value and is widely recognized by experts in dynamical systems as one of the significant long-standing open problems in the field, serving as a litmus test for mathematical reasoning capabilities.
The related paper has been published on the preprint platform arXiv, and its formalization code is available on GitHub. Links provided by IT Home are as follows:
https://github.com/frenzymath/HolomorphicAnosov
The Shanghai AI Laboratory stated that the significance of this research also lies in validating a new scientific research paradigm. Traditional mathematical research relies on the prolonged exploration of individual geniuses, whereas this breakthrough systematically integrated expert intuition into the machine-solving loop, forming a closed cycle of "systematic exploration — expert judgment — result accumulation — feedback correction." This paradigm can be replicated and extended to more fundamental research fields characterized by "vast search spaces and scarce experts," enabling further "zero-to-one" original innovations.
Moving forward, leveraging the complete capability loop established in this study, the team will package it into a reusable mathematical verification module within the Shusheng · Duan Yan Scientific Discovery Platform, allowing direct invocation for subsequent scientific problem research. Simultaneously, using the breakthrough on the three-dimensional Ghys conjecture as a starting point, the Shanghai AI Laboratory will extend its accumulated reasoning capabilities to other disciplines sharing similar mathematical structures; upon achieving new breakthroughs, these new reasoning capabilities will be packaged back into the Duan Yan platform for reuse, combined with more disciplines to seek the next round of breakthroughs, thereby creating a self-evolving flywheel of "breakthrough — packaging — reuse — re-breakthrough."