对话许地生、张洁松：人机协作，如何攻克一个困扰数学界30年的猜想？

李璐｜撰文

陈晓雪｜编辑

团队成员瑞典皇家理工学院张洁松博士在项目完成过程中起重要作用。北京大学董彬教授、刘若川院士团队利用其开发的SHEAF框架对本次证明完成形式化验证，验证了这一工作的正确性。

过去30余年，数学家从不同方向探索这一猜想，却始终没有解决其三维情形。许地生此前也曾与合作者研究这一问题，但没有找到有效的证明思路。

相关论文《Codimension-one holomorphic Anosov diffeomorphisms》于9月29日在预印本网站arXiv上发布，10月13日完成最后一次更新[1]。论文由张洁松单独署名。他在论文中感谢自己的博士导师许地生与他持续讨论三维Ghys猜想，并促使他作为访问学者在上海人工智能实验室中工作，研究的主要思想正是在这一阶段形成的。

许地生是此次研究项目的发起人，他参与了模型的前期训练，并负责设计研究计划、整合资源，以及与北大团队联系合作事宜。考虑到张洁松在完成证明和撰写论文过程中承担了主要工作，两人最终选择遵循传统数学界的署名原则，让这篇数学论文由张洁松单独署名。

许地生告诉《赛先生》，当他看到AI尝试在复几何的框架下证明Ghys猜想时，意识到其中可能存在值得继续探索的方向，他随即邀请张洁松加入研究，团队在与AI的多轮交流中，逐步找到了一条可行的证明路径。

关键突破来自AI帮助将三个不同的数学工具联系了起来，而这三个工具对于数学家来说并不陌生。此后，解决这一问题有了新的可能。

1995年，法国数学家艾蒂安·吉斯（Étienne Ghys）提出了一个关于复流形与动力系统的猜想。它试图回答一个问题：一个具有特定混沌运动特征的复流形，其几何结构是否受到严格限制，最终可以归结为一类具有明确代数结构的标准模型？

Ghys猜想认为，每个紧致复流形上的全纯Anosov微分同胚，都与某个复infra-幂零流形上的仿射自同构双全纯共轭。

Anosov微分同胚由俄国数学家德米特里·阿诺索夫（Dmitri Anosov）提出。在一个紧致、无边界的流形上，每一点的切空间都能分为稳定和不稳定两个互补部分，并可以在变换下维持。随着不断迭代，稳定方向上的微小偏差以指数级速度缩小，不稳定方向上的偏差则以指数级速度放大，而这种收缩与扩张具有空间一致性。Anosov微分同胚是动力系统领域的一个中心研究对象，是一类经典的混沌系统。

Ghys猜想研究的是紧致复流形上的全纯Anosov变换。“全纯”意味着描述系统演化的映射在局部复坐标下具有复可微性。猜想断言，原流形与某个复infra-幂零流形之间存在全局的一一对应，其中对应映射及其逆映射都全纯。在这一对应下，原来的Anosov变换可以表示为后者这一具有严格代数规则的复空间上的仿射自同构。

北京大学北京国际数学研究中心谢俊逸教授评价道，“Ghys猜想的难点在于，它对应的实（数）版本的类似断言仍是著名的难题，复数的情形问题变得更加刚性，是复动力系统刚性现象研究中的重要问题，非常困难”。

许地生、欧阳泽轩与张洁松三人共同讨论学习过雷恩数学研究所主任塞尔日·坎塔（Serge Cantat）在2004年发表的论文，在欧阳泽轩的解释帮助下，论文中与复几何相关的技术给他们留下了深刻的印象。但许地生表示，由于自己当时并不熟悉这个领域的一些重要技术，因此并未能成功的应用到三维Ghys猜想的证明中。

张洁松告诉《赛先生》，当时作为博士研究生，他很难处理横截方向维数较高的叶状结构的正则性问题。他解释说，在每一片叶子内部，动力系统提供了丰富的信息，因此比较容易得到良好的正则性。但真正的困难在于“横截方向”，也就是从一片叶子移动到另一片叶子时，自己很难理解叶状结构如何变化，才能使相应方向随位置的变换符合全纯性的要求。

Ghys的方法可以处理横截方向为复一维的情形，而在更高的复维数中，全纯性与共形性不再等价，这条路径无法直接推广。

尽管如此，许地生和张洁松还是在邻近方向上取得进展。两人合作了《On holomorphic partially hyperbolic systems》，证明了“纤维化”全纯部分双曲系统的中心分布是全纯的，发表在数学顶尖期刊欧洲数学会杂志JEMS。[2]

“我们当时认为这项成果后续可以用于研究一些特殊情形的三维Ghys猜想，但距离完整解决猜想仍有差距。”许地生说。

但竞赛成绩不等同于数学研究能力。许地生在接受《赛先生》采访时表示，竞赛与研究所涉及的知识、学科乃至思维深度和广度都有差别。所以很多优秀的竞赛选手仍需要进入大学进行大规模的学习，才能做出很好的科研工作。

当时，上海人工智能实验室也开始探索模型从竞赛级数学向研究级数学迈进。双方不谋而合。

2026年初，许地生与上海人工智能实验室正式启动模型训练合作研究。许地生提到，他参与筛选书生-S2模型的训练语料，并结合科研经验指出模型与系统的能力短板。

7月底，团队开始大规模地测试各类数学题目。许地生注意到模型处理复杂数学命题的能力实现了质的提升，便将Ghys猜想也纳入尝试。

针对三维Ghys猜想，书生-S2首轮生成了400页的推导报告。

许地生告诉《赛先生》，令他印象深刻的是，AI尝试在复几何假设下证明Ghys猜想。他从中看到了推进证明的可能性。

随后，已经前往瑞典皇家理工学院开展博士后研究的张洁松受邀加入团队。他坦言，自己在收到邀请时，更多是抱着试一试的心态，想看看AI能否带来一些新的思路。

回顾最终的突破，他将其称为“意外之喜”

如果要推广此前的论证，就需要把这两个方向以足够好的方式“粘合”起来，问题又回到了此前曾困住他的叶状结构正则性上。

突破来自几个已有数学工具的结合。

张洁松向《赛先生》解释，这项证明沿用了动力系统中通过bunching 估计研究叶状结构正则性的经典思路。这类方法通常需要不同方向上的膨胀与收缩速率满足额外的逐点条件，才能保证所需的导数估计随迭代衰减。

此次证明的突破在于，复几何结构使研究者能够在L²积分意义下得到这种衰减，并进一步将其强化为逐点的正则性讨论，从而绕开通常所需的额外假设。

具体来说，在复余一维结构下，研究者可以用一个随迭代次数指数衰减的因子，乘以相应迭代的实Jacobian，来控制相关反全纯导数的平方。这里恰好可以利用一个简单的换元积分事实：将流形的总体积归一化为 1 后，微分同胚每次迭代的 Jacobian 积分都等于 1。因此，对上述估计积分后，便能得到反全纯导数在 L² 意义下的指数衰减，进而证明所需的正则性。

这正是AI在这项工作中发挥关键作用的地方。“真正不容易的，是想到将复几何提供的特殊结构、经典的bunching 估计思路与这一基本的积分事实结合起来。”张洁松说。

上海人工智能实验室公布的记录显示，书生-S2先后完成7批接续推演，问题图（Problem Graph）从15个节点扩展到389个，输出总量达千页的严密推导，同时生成数十种全新论证思路。

“首先要做的是理解证明，并确认每一步推理都是正确的。”张洁松说。在完整证明形成之前，他与AI进行了多轮交流和反馈，一边核查模型的推理步骤，一边引导它调整和完善思路。

分散在多轮人机交互中的论证过程，需要使用人类易于理解的语言撰写证明过程，并整理成可被同行阅读、验证以及审查的文本。

张洁松告诉《赛先生》，AI给出的思路虽然在数学上成立，但表达和组织方式往往不便于人类理解。因此，他需要重新梳理论证的脉络，用标准的数学语言把这些思路组织成便于读者理解和检验的证明，进而完成论文的撰写。

许地生还意识到，“AI For Math是新的科研范式，我们可能需要新的方法来验证命题的正确性。”

因此，许地生联系了北京大学董彬教授和刘若川院士团队，希望他们可以帮忙为此次证明进行形式化验证。他记得董彬教授2022年就在北京国际数学研究中心做过一个报告，关于如何运用人工智能辅助数学中几何拓扑研究。

许地生回忆，当时董彬刘若川团队他们正在攻关收尾关于庞加莱猜想证明的形式化，但他们还是非常支持这项合作。最终，团队决定使用自主开发的SHEAF框架，对论文的四个四个主定理进行Lean形式化验证。经过近半个月的工作，他们成功完成了验证。

回顾这次经历，张洁松表示，AI在生成证明和形式化验证等环节中发挥重要作用，这可能对数学家在提出问题、理解数学、发展理论和探索应用等方面提出更高的要求。他也强调，数学是人类文化的一部分，一套数学理论的提出、完善，以及对它的理解和运用，始终需要人的参与和把关。

许地生认为，这次团队合作的意义不仅在于证明了悬而未决的猜想，更重要的是探索了AI进入数学领域后，引发的科研范式的革新，各领域数学家如何在AI辅助下协作。“数学论文不再是唯一产出，还会有关于AI的论文、形式化验证、模型更新迭代、甚至是报告讲解视频材料等，均可作为新时代（AIx数学）的科研的产出。”

“希望这次工作能够起到抛砖引玉的作用，为数学家在AI时代开展数学研究，提供一点参考和经验。”张洁松告诉《赛先生》。

那么，如果AI未来能够解决数学界的大部分猜想，人类是否还会继续从事数学研究吗？对此，许地生的回答是：“数学是人类思维训练中非常重要的组成部分，从这个角度来说我会永远待在数学，特别是数学教育这个领域的。”

参考文献：

[1] https://arxiv.org/abs/2609.37695

[2] http://ems.press/journals/jems/articles/14299208

[3] https://www.shlab.org.cn/news/5444307