书生-S2多模态大模型助力中国团队完成三维Ghys猜想证明并通过Lean形式化验证

许地生团队依托上海AI实验室的书生科学多模态大模型S2，通过人机协同完成困扰数学界30余年的三维Ghys猜想证明，论文已发布在arXiv，形式化代码公开于GitHub。书生-S2完成7批接续推演，问题图从15个节点扩展到389个，输出上千页推导；北大董彬、刘若川团队用自研SHEAF框架在约5天内完成全部四个主定理的Lean形式化验证，产出约55万行代码。