[技术] 上海 AI 实验室「书生-S2」助阵，三维 Ghys 猜想被证明并通过 Lean 形式化验证

上海人工智能实验室访问学者、大湾区大学教授许地生团队，依托书生科学多模态大模型 S2，基于「通专融合」路径、通过人机协同完成了三维 Ghys 猜想的证明。北京大学董彬教授、刘若川院士团队用其自研 SHEAF 框架对论文四个主定理完成形式化验证，证明通过 Lean 检验。

Ghys 猜想由法国数学家 Étienne Ghys 于 1995 年提出，是复动力系统领域的长期公开难题之一。通俗点说，它问的是：一个「运动方式足够混沌」的复流形世界，是否只能长成复环面这类高度规整的形状。北大的谢俊逸教授评价，这道题的实数版本至今仍是完全公开的难题，复数情形更刚性、更难。

攻关过程里的几个数字挺能说明 AI 在这类题上的定位。针对三维 Ghys 猜想的首轮推理，书生-S2 就产出了 400 页推导报告；整个过程完成 7 批接续推演，问题图从 15 个节点扩展到 389 个，输出总量上千页，还生成数十种全新论证思路。数学家负责把握方向、判断哪些思路值得深挖，模型负责铺开海量繁琐推导，靠多轮对话反复迭代。

关键的是最后那步验证。北大团队约 5 天完成全部四个主定理的形式化，峰值并发达 100 个智能体，产出约 55 万行 Lean 代码。论文已上传 arXiv，形式化代码在 GitHub 公开。有意思的是，动力系统专家谢俊逸此前用 GPT-6 试过同一道题，并没有找到证明方案。

原文链接：https://www.leiphone.com/category/academic/ChIK9FvwSwlHmfFc.html
来源：雷峰网