Shanghai AI Laboratory’s Shusheng-S2 Helps Prove the Three-Dimensional Ghys Conjecture
Xu Disheng’s team used Shanghai AI Laboratory’s Shusheng-S2 model in a human–AI collaboration to prove the three-dimensional Ghys conjecture, with a preprint posted on arXiv. Researchers guided seven rounds of recursive exploration as the problem graph expanded from 15 to 389 nodes. A Peking University team used its SHEAF framework to formalize all four main theorems, producing approximately 550,000 lines of Lean code in about five days and passing Lean checks.
Why it matters: The workflow offers a transferable approach to research mathematics, pairing expert guidance with recursive model exploration and organizing formal verification around a dependency graph of checkable proof tasks.