The research team, led by Xu Disheng, a visiting scholar at the Shanghai Artificial Intelligence Laboratory, has successfully proven the three-dimensional Ghys conjecture—a problem that has eluded mathematicians for more than three decades. They achieved this through human-machine collaboration using the InternLM-Sci scientific multimodal large model S2. Meanwhile, the team of academicians Dong Bin and Liu Ruochuan from Peking University employed the SHEAF framework to conduct a formal verification of the proof, confirming its validity. This achievement marks the first instance where Chinese scientists have harnessed a domestically developed large model to solve a world-class mathematical problem. The relevant research paper has been published on a preprint platform, and the formal verification code has also been made publicly accessible.
This study not only demonstrates the power of integrating expert intuition with machine-solving capabilities but also validates a new scientific research paradigm. This approach can be applied to more fundamental research fields characterized by vast search spaces and a scarcity of experts. Moving forward, the team plans to encapsulate the relevant capabilities into a mathematical verification module for the InternLM-Duanyan Scientific Discovery Platform. They aim to gradually extend these capabilities to other related disciplines, thereby forming a self-evolving mechanism.
