Shanghai AI Lab uses large model to solve 30-year-old Ghys Conjecture

A research team led by Professor Xu Disheng from Greater Bay Area University, acting as visiting scholars at the Shanghai AI Laboratory, has successfully proven the three-dimensional Ghys Conjecture. This mathematical problem, proposed by French mathematician Étienne Ghys in 1995, has remained unsolved for over 30 years and is considered a significant challenge in the field of dynamical systems.

The breakthrough was achieved using the Shushen-S2 (书生-S2) scientific multimodal large model through a human-AI collaborative approach. The process involved a “specialized-general integration” technical path where the AI performed large-scale recursive reasoning and complex derivations while human experts provided strategic direction and intuitive feedback. The model produced extensive derivation reports, which helped expand the problem's logical nodes from 15 to 389.

To ensure the accuracy of the findings, a team from Peking University led by Professor Dong Bin and Academician Liu Ruochuan utilized the SHEAF framework to perform formal verification. The proof was successfully validated using Lean, generating approximately 550,000 lines of code. This achievement marks the first time Chinese scientists have used a domestic large model to solve a world-class mathematical problem, signaling a new research paradigm that integrates expert intuition with machine-driven exploration.