Shanghai AI Lab's Intern-S2 helps prove the three-dimensional Ghys conjecture, verified in Lean

Shanghai AI Laboratory says its Intern-S2 scientific multimodal model helped mathematicians prove the three-dimensional case of the Ghys conjecture, posed by Etienne Ghys in 1995.

A Peking University team then formalized the main results in Lean using SHEAF, an open-source formalization agent, producing about 550,000 lines of Lean code in roughly five days.

The source says the paper's sole listed author, Jiesong Zhang, used an internal Intern-S2 version and independently verified all the mathematics.