整理：TopAIMap 编辑
上海 AI 实验室书生 Intern-S2 参与证明 30 年三维 Ghys 猜想：7 轮人机迭代、问题图从 15 扩到 389 节点，北大 SHEAF 用 100 个 agent 5 天完成 Lean 验证
上海人工智能实验室 10 月 15 日公布，数学家许地生、张介松与书生 Intern-S2 多轮协作，证明了 1995 年提出的 Ghys 猜想的三维（余维一）情形；北京大学团队用 SHEAF 框架在 Lean 中形式化验证了全部四个主定理。
10 月 15 日，上海人工智能实验室发布成果：困扰数学界 30 余年的三维 Ghys 猜想（1995 年由法国数学家 Étienne Ghys 提出，属复动力系统）在人机协作下被证明。论文已上 arXiv（2609.37695，《Codimension-one holomorphic Anosov diffeomorphisms》），作者 Jiesong Zhang（张介松），结论是：紧连通复流形上的余维一全纯 Anosov 微分同胚都双全纯共轭于复环面上的双曲自同构——即验证了 Ghys 猜想的余维一情形，特别是复三维情形，而非完整猜想。作者在文中声明 Intern-S2 通过多轮对话辅助生成思路，所有论证由本人独立验证负责；访问学者许地生参与讨论。
过程数字（据实验室在知乎的一手复盘）：Intern-S2 首轮探索产出一份约 400 页的报告，两位数学家从中挑出有希望的方向、否掉死胡同、反复给系统改方向；7 轮迭代后，问题图从 15 个节点扩到 389 个，突破来自这个反馈回路，而不是一次提示或模型自主运行。形式化环节由北大刘若川团队用 SHEAF 框架完成：把定义、命题、依赖关系整理成有向无环图分发给多个 agent，最多 100 个并发、约 5 天，四个主定理全部通过 Lean 检查，并由专家核对形式化陈述与论文一致；形式化代码已公开。
谁能用：Intern-S2 系列权重已在 Hugging Face 开放，最新的 internlm/Intern-S2-397B-FP8 为 Apache-2.0 许可（社区指出其底座为 Qwen 3.5-397B-A17B 后训练），需要自备多卡算力部署；此次用于数学研究的「研究 harness」实验室称后续会封装进书生·端砚科学发现平台，目前未公布开放方式或价格。
解读：这件事真正的新闻点不是「国产大模型独立攻克难题」——论文作者自己就说清了是人主导、AI 扩搜索——而是给出了一套可复制的科研流水线：模型铺开候选路线，专家剪枝，再用多 agent 做形式化验证兜底。「5 天、100 个 agent 跑完 Lean 验证」比证明本身更可能改变数学界的工作方式。 讨论：1. 当 AI 产出 400 页候选思路、人类负责挑选，论文署名和贡献应该怎么划分？2. 形式化验证成本降到「几天」量级后，期刊审稿会不会开始要求附带 Lean 证明？
