一个悬置三十年的猜想、一个中国模型，与一份经机器验证的证明

一个悬置三十年的猜想、一个中国模型，与一份经机器验证的证明

10月15日，Shanghai AI Laboratory（上海人工智能实验室）宣布，一支研究团队证明了 Ghys 猜想的三维情形——这是动力系统中一个自1995年起悬而未决的公开问题。相关工作由该实验室自有的 Intern-S2 模型推进，最终完成的证明由 Peking University（北京大学）的团队在 Lean 中完成形式化验证。

其意义不只是一道难题被攻克。更在于这次发布围绕的是过程而非某个数字：模型给出推导，研究者决定把注意力投向哪几条进攻路线，证明助手则逐步核验每一个环节。这套组合正是业界过去两年反复承诺的东西，如今它终于配上了一篇论文。

这个猜想问的是什么

Étienne Ghys 于1995年提出该问题。大致来说，它问的是：混沌动力系统的行为能否决定其几何分类——换个说法，就是运动能否告诉你它所在空间的形状。

被解决的并不是那个一般性问题。团队证明的是余维一情形，也就是三维情形，它在三十年间一直悬而未决。这一区分对诚实理解该声明很重要：完整猜想仍然更宽泛，但那个此前难倒所有人的特定情形，如今已经落定。

第一轮就产出了四百页

这次协作的具体机制比结果本身更有意思，因为它展示了人机科研在每一分钟里实际上是什么样子。

Intern-S2 对该问题的首次探索产出了一份约400页的推演报告。那不是答案，而是一堆候选推理，其中一些有用、一些没用——当你让模型去思考一个真正未解的问题，而不是回忆已知的东西时，得到的正是这种形态的产出。

此后，工作又经过七轮持续推理。问题图——即子命题及其相互依赖关系的图谱——从15个节点扩展到389个。累计产出约达一千页，涵盖数十种不同思路。在每一个阶段，数学家都做了模型自己做不到的事：审视这些提案，判断哪些突破口有希望，并引导下一轮方向。

实验室访问学者、Greater Bay University 教授 Xu Disheng，以及自博士阶段起便一直追踪该猜想的博士后研究者 Zhang Jiesong，提供了这种判断力。Zhang 的论文于9月29日发布到 arXiv，10月13日修订，是一篇单作者论文，并附有 AI 使用声明：模型通过多轮对话协助发展了思路与论证，而他对数学部分做了独立核验。

让它不止是一个故事的部分

关于 AI 解决数学问题的说法很廉价。这一次之所以有分量，在于证明被形式化了。

由 Bin Dong 和 Ruochuan Liu 领衔的 Peking University 团队，用其自有的 SHEAF 框架，把四个主要定理，以及论证所依赖的 Ghys 支撑性结果，全部加以形式化。形式化意味着把定义、假设和推理翻译成计算机可以检查的语言——写作者的每一步论证都必须被明确写出，而不能留给受过训练的读者去补全。

这项工作大约花了五天，最多时有100个 agent 并行工作，产出约55万行 Lean 代码。Lean 是一个交互式定理证明器。它不在乎谁有多自信。它检查逻辑，要么接受这份证明，要么不接受。

SHEAF 把任务组织成由定义、命题和依赖关系构成的有向图，使不同的 agent 可以处理相互连接的片段，同时团队追踪哪些陈述已有证明、哪些仍需要。这是一种真正新型的分工方式；该框架还必须修补现有动力系统形式化库中的空缺，因为这份证明所需的工具链当时根本还不存在。

人与模型，各司其职

实验室描述的这套分工值得照单全收，因为它对双方都不是那种好听的说辞。

模型负责检索文献、把命题拆解成小块、并行探索证明分支、检查逻辑步骤，并快速测试大量想法。人负责定方向、判断哪些路径值得追求，并做出决定下一轮精力投向何处的取舍。

这两半截然不同。模型的贡献在规模与耐力：它能同时记住几十条死胡同而不气馁。人的贡献是品味，也就是能从一百页看似合理的推理中，看出哪三段才是关键的能力。

这里还附着一则中国媒体大加渲染的趣闻。据报道，一位动力系统专家在听说国内某模型解决了该问题后，出于好奇把同样的问题抛给了 GPT-6，结果它没能做到。狭义地看，这只是两个系统在同一个问题上的比较，说明不了太多。若作为竞争态势的信号来读，它正是那种会驱动投资的细节。

为什么形式化验证改变了赌注

过去两年的大多数时间里，AI 辅助数学的瓶颈并不在于生成候选论证。模型擅长产出看似合理的推理。瓶颈在于判断其中哪些是正确的，因为检查一份证明既慢、又依赖专家，还难以并行化。

Lean 把这一点反了过来。一旦某个陈述被形式化，验证就变得廉价而快速，而且值得信赖，因为它靠的是机械流程而非社会共识。55万行才是昂贵的部分，而一个团队加上一百个 agent 能在五天内产出它们，才是这里真正的进步。它暗示：当生成这一端的瓶颈早已松动时，验证这一端的瓶颈或许也正在放宽。

实验室表示，会把该工作流打包为其科学发现平台上的可复用数学验证模块，把模型、agent、数据与实验设备连接起来。它还提到一项更早的成果：Wuhan University（武汉大学）的一支团队曾用该平台，把某个电化学合成工艺的研发周期从五到十年缩短到一到两年。

可以从中读出什么

诚实的总结是：这是一个真实的结果，有真实的证明，而产出它的工作流仍然高度依赖人力。七轮专家引导，并不是一个模型在自行运转。一篇附有 AI 使用声明的单作者论文，也不是模型在邀功。

发生变化的是，这个闭环现在合上了。模型能在一个无人解决的问题上产生足够分量的推理，人能引导它，而证明助手能认证结果，无需任何人去信任一份摘要。这是一条流水线，而不是一次演示；而正是一条条流水线，把一项能力变成一种实践。

下一个问题是：这是否能推广到那些根本无法形式化的情形之外。几何与动力系统具有某些适合机器检查的结构。而科学的其余大部分并不如此；恰恰是在生物学、材料与医学这类更混乱的领域，AI 作为研究助手的承诺才会真正受到检验。Ghys 的结果说明这件工具能用。它还没有说明能有多常用。