上海AI实验室书生-S2 助力三维 Ghys 猜想证明并通过形式化验证

上海人工智能实验室访问学者许地生团队依托书生科学多模态大模型 S2（书生-S2），通过人机协同完成三维 Ghys 猜想证明，北京大学董彬、刘若川团队用 SHEAF 框架完成形式化验证并通过 Lean 检验。