书生-S2大模型助力三维Ghys猜想证明并通过形式化验证

上海AI实验室书生-S2大模型与许地生团队人机协同完成三维Ghys猜想证明，输出上千页推导和数十种论证思路，北大董彬、刘若川团队用SHEAF框架在Lean系统中完成形式化验证，验证耗时约5天、产出55万行代码。相关论文已发布于arXiv，形式化代码公开于GitHub。该工作标志着中国大模型首次攻克世界级数学难题，验证了AI在前沿数学研究中的推理与协作能力。