Shanghai AI Lab's Shusheng-S2 helps prove a three-dimensional Ghys conjecture result
Original title (Chinese)
上海AI实验室“书生-S2”大模型进入前沿数学研究流程：助力三维Ghys猜想证明并通过形式化验证
Shanghai AI Laboratory and Professor Xu Disheng's team say the Shusheng-S2 scientific multimodal model, working with human researchers, produced a proof of the three-dimensional Ghys conjecture.
Peking University's Dong Bin and Liu Ruochuan team says it completed a Lean formal verification of all four main theorems in about five days, producing roughly 550,000 lines of Lean code.
The collaboration ran seven rounds of recursive reasoning, growing the problem graph from 15 to 389 nodes.
The article details how humans and the Shusheng-S2 model worked iteratively on a three-dimensional Ghys conjecture result, and how Peking University verified it in Lean.
Source: Leiphone · leiphone.comPublished · added here