书生-S2助力完成三维Ghys猜想证明并通过Lean形式化验证

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