联合团队借助书生-S2大模型完成三维Ghys猜想证明与形式化验证

大湾区大学许地生团队依托上海人工智能实验室书生-S2大模型，通过人机协同证明了三维Ghys猜想，相关论文已在arXiv发布。攻关过程中书生-S2通过多轮推演输出了千页推导报告并生成全新论证路径，随后北京大学团队利用SHEAF框架调度最高100个智能体，耗时约5天产出约55万行Lean代码完成全部主定理的形式化验证。