上海 AI Lab 称书生-S2 协助证明三维 Ghys 猜想，北大完成 Lean 形式化
上海 AI Lab 10 月 15 日公布三维 Ghys 猜想证明进展：论文作者称 Intern-S2 协助发展思路，北大团队用 Lean 完成形式化。
三维 Ghys 猜想是关于复流形上全纯 Anosov 微分同胚的猜想；上海 AI 实验室（Shanghai AI Lab）10 月 15 日宣布研究团队给出证明。arXiv v3 列出的唯一作者 Jiesong Zhang 在 AI 使用声明中写道，他使用内部版书生-S2（Intern-S2）通过多轮对话协助发展文中的数学思想和论证，并独立核验全部数学论证、对稿件承担全部责任。北大团队另用 Lean 对相关定理作形式化验证，代码公开在 GitHub。
要点
- arXiv 论文的定理针对紧致连通复流形上的余维一全纯 Anosov 微分同胚，结论是它与复环面上的双曲自同构双全纯共轭。
- 上海 AI Lab 公告称，探索阶段从 15 个问题节点扩展到 389 个，首轮输出约 400 页；团队经过 7 轮推理批次形成证明路线。
- 上海 AI Lab 公告与钛媒体均称，北大团队形式化约用 5 天、峰值并行 100 个 agent，产出约 55 万行 Lean 代码。
三维 Ghys 猜想
相关猜想由 Ghys 于 1995 年提出。这里的“三维”指论文研究的复几何问题，主定理还要求流形紧致、连通，映射全纯且余维为一。上海 AI Lab 将这项工作称为书生-S2 参与解决世界级数学开放问题；arXiv v3 的 AI 使用声明则具体写明，唯一作者 Jiesong Zhang 使用内部版 Intern-S2 协助发展文中的数学思想和论证，并独立核验数学论证、对稿件负责。
这项新闻包含三类不同材料：arXiv v3 的作者声明说明 Intern-S2 如何参与；上海 AI Lab 公告提供项目探索过程；GitHub 仓库列出 Lean 形式化的目标定理和前提。项目方公布的流程指标不能代替数学论证，代码规模也不能代表模型的贡献大小。想了解其他 AI 数学报道，可参阅本站的 AlphaProof Nexus 和 OpenAI 公开 AI 数学稿件；它们是不同事件，不作为本案论据。
证明进展
上海 AI Lab 公告称，合作研究于 2026 年初启动，团队从当年 8 月起开始从多个角度探索猜想；钛媒体另报道称，许地生于 3 月成为上海 AI 实验室访问学者，书生-S2 及配套系统在 8 月内部迭代成型。官方公告称，初期生成约 400 页材料，随后经历 7 轮推理批次；问题图从 15 个节点扩至 389 个，累计产出数千页推导和多条证明尝试。数学家负责判断路线、筛选思路并给出反馈，模型承担大规模推演。上述页数、节点数和时间线是项目方公布的过程信息，不能单独证明数学结论正确。
arXiv v3 的 AI 使用声明以单数写明，唯一作者 Jiesong Zhang 使用内部版 Intern-S2 通过多轮对话协助发展文中的数学思想和论证；声明还说 Zhang 独立核验了全部数学论证，并对稿件承担全部责任。公开声明没有逐条归因具体引理，因此不能据此把整体证明贡献归给模型。
形式化验证
形式化部分提供了另一种核查路径。北大董彬、刘若川团队使用 SHEAF 框架，把论文中的定理和依赖关系拆成 Lean 命题，再由并行 agent 推进证明；最终代码放在 frenzymath/HolomorphicAnosov。仓库 README 列明形式化涵盖 Theorem A 与 Theorems 1.1、1.2、1.3，称这些定理的证明没有 sorry，且 Lean comparator 可接受其解答。上海 AI Lab 与钛媒体均将代码规模概述为约 55 万行 Lean；仓库 README 未给出精确行数，因此这里不列精确统计。
有一个需要准确说明的前提：Theorems A、1.1 和 1.3 把 HomotopyTorusRigidity 列为假设；README 将它称为环面情形的 Borel 猜想，并指出 Hsiang 与 Wall 在 1969 年已证明。这是论文及形式化陈述中的经典数学输入，不是 Lean 证明遗漏或未完成的结论。Theorem 1.2 不需要这一假设。读者审查代码时，应把“证明了哪些定理”和“哪些经典结果作为前提”一起看。
| 项目 | 公开材料中的信息 |
|---|---|
| 论文结论 | 余维一全纯 Anosov 微分同胚与复环面双曲自同构双全纯共轭 |
| 模型角色 | 论文作者称内部版 Intern-S2 协助发展证明思路 |
| 形式化对象 | Theorem A、Theorems 1.1、1.2、1.3 |
| 工程规模 | 约 5 天、峰值 100 个 agent；项目方称约 55 万行 Lean |
| 明示前提 | Theorems A、1.1、1.3 采用 HomotopyTorusRigidity；1.2 不采用 |
如何核对
想在一分钟内判断这是不是一条有代码支撑的数学新闻，可以先打开论文摘要和代码仓库 README：论文给出命题及 AI 使用声明，README 列出形式化覆盖范围、Lean 版本和前提。要继续验证，仓库说明的本地步骤是先获取 Mathlib 缓存，再构建项目：lake exe cache get、lake build；如需对照锁定后的定理陈述，还可按 README 执行 comparator 命令。Lean 工具链为 leanprover/lean4:v4.35.0-rc1，缺少对应依赖时，构建并非一条命令就能跑通。
公开仓库可用于核对形式化目标和代码；arXiv 页面将论文列为预印本。此次查阅的材料没有提供同行评审或数学界接受度的结论，因此本文不据此判断论文是否已获学界认可。代码中的无 sorry 也不意味着所有先决假设都在此仓库中重新证明，HomotopyTorusRigidity 的位置正好说明了这一点。
编辑判断
这项工作的价值不只在模型参与研究，而在于把论文论证和 Lean 形式化代码并列公开：读者可以分别追问模型实际贡献了什么，以及数学结论如何被编码、依赖哪些前提。它也提供了一个相对具体的 AI+数学案例，显示生成式探索与形式化验证可以由不同团队、不同工具链承担。
对研究者和 AI 工具开发者，这个案例值得观察的是模型辅助的数学探索如何与形式化验证衔接。Lean 检查针对的是代码中定义和证明的命题，不会自动回答论文表述是否对应研究者希望表达的数学内容。arXiv 将论文列为预印本；此次查阅的材料没有给出同行评议或学界接受度结论。