上海AI实验室书生-S2与数学家合作证明Ghys猜想，北大团队5天完成55万行Lean代码验证

大湾区大学许地生团队与上海AI实验室用书生-S2科学基础模型证明了1995年提出的Ghys猜想在复余维一情形下成立，解决了悬而未决30多年的复三维情形。模型经7批接续推演，问题图从15个节点扩展到389个节点，累计生成上千页材料。北京大学董彬、刘若川团队随后用Lean 4和自研SHEAF框架，在约5天内生成约55万行Lean代码，完成论文四个主要定理的形式化验证，代码已在GitHub公开。