一项1995年的数学问题取得新进展
一项于1995年提出的数学猜想，如今已有一项证明涵盖复维数三的情形。这项成果来自数学家与上海人工智能实验室 Intern-S2 模型的合作。随后，北京大学团队将论文的四个主要定理转化为由 Lean 验证的证明。Lean 是一套用于检验数学推理的计算机系统。
目录
上海人工智能实验室于2026年10月15日宣布了这一成果，并介绍了由许笛声教授领导的团队。许笛声任教于大湾区大学，同时是该实验室的访问学者。研究论文《余维一全纯阿诺索夫微分同胚》的唯一作者是瑞典皇家理工学院的张杰松。
这一结果解决了法国数学家埃蒂安·吉斯猜想的余维一情形，其中包括复维数三的情形。该猜想涉及运动与形状之间一种引人注目的关系：如果一个空间能够承载某种特定的混沌运动，那么它本身是否必定具有高度有序的数学结构？
Intern-S2 通过与研究人员反复交流，帮助发展思路和论证。张杰松在人工智能使用声明中表示，他独立核查了全部数学内容。这项合作结合了机器探索、人类判断以及独立的形式化验证流程。
该实验室称，这是中国人工智能模型首次助力解决如此重要的数学问题。具体成果是一项分类定理，并附有公开的预印本和已公开发布的形式化代码。
证明揭示的运动与形状关系
吉斯猜想属于复动力系统领域，研究的是坐标遵循复数规则变化时数学系统如何演化。复数有两个实数分量，因此复维数三在局部对应六个实维度。这里的数学环境比普通物体在房间里移动抽象得多。
阿诺索夫系统具有精确的拉伸与挤压组合。在反复运动中，某些方向收缩，另一些方向扩张。起点相近的轨迹可能迅速分离，从而产生混沌行为，尽管每一步的演化规则都十分精确。
可以把它想象成一个反复拉伸并折叠形状的过程。但这里研究的数学系统有严格得多的限制：拉伸和收缩必须满足一致的条件，而且运动必须保留复坐标所赋予的结构。
吉斯猜想认为，紧致复流形上的此类系统应当具有标准的代数描述。流形是一种空间，尽管整体形状可能复杂，但在小范围内看起来很简单。在这里，紧致性是一种数学条件，意味着空间不会无限延伸。
张杰松的定理表明，紧致连通复流形上的每个余维一全纯阿诺索夫微分同胚，都与某个复环面上的双曲自同构全纯共轭。通俗地说，经过一种保留复结构的可逆坐标变换，原有运动可以转化为一个非常规整空间上的标准代数变换。
复环面可以通过将复空间中相差一个重复格点的点视为同一点来构造。核心成果在于，复杂的动力学迫使空间呈现这种有序的几何描述。
为何定理的适用范围很重要
这篇论文研究的是余维一情形。对于这类系统，意味着收缩或扩张部分中有一部分的复维数为一。该定理一般性地涵盖了这一受限类别，并解决了复维数三的猜想情形。
吉斯更广泛的猜想涉及更大范围复流形上的全纯阿诺索夫系统，并用称为复殆幂零流形的空间上的标准代数模型描述这些系统。张杰松的结果为所研究的情形给出了一个特别严格的答案：复环面和双曲自同构。
对于研究这一问题的数学家而言，该定理将问题从寻找未知的空间与运动，转变为研究一个标准模型。坐标变换将原系统与该模型联系起来，同时保留复几何结构。
许笛声多年来一直在研究这一问题。他此前曾与自己的前导师、菲尔兹奖得主阿图尔·阿维拉共同研究三维情形。许笛声和张杰松后来取得了相关的部分结果，并发表于《欧洲数学会杂志》。这项新研究建立在他们对同一数学问题的持续关注之上。
从奥林匹克竞赛测试到研究合作
Intern-S2 的参与建立在 Intern-S1 此前在2025年中国数学奥林匹克竞赛中取得的成绩之上。中国数学会负责中学数学竞赛的委员会当年组织了一场人工智能测试，邀请三个中国模型在与人类参赛者相同的时限内解题。
按照相同的评分标准，Intern-S1 得了102分，在三个参赛模型中排名第一。金牌分数线为78分，因此它高出24分，约高出31%。
许笛声看到了在研究数学中使用这一系列模型的潜力，上海人工智能实验室则希望从竞赛题拓展到尚未解决的问题。双方于2026年初开始合作，并搭建了一套称为 Harness 的软件系统，用于组织模型的工作及其与研究人员的交流。
主要进展如下：
- 1995年：埃蒂安·吉斯提出该猜想。
- 2025年：Intern-S1 在中国数学奥林匹克人工智能测试中取得102分。
- 2026年初：许笛声与上海人工智能实验室开始模型训练合作。
- 2026年3月：许笛声成为该实验室的访问学者。
- 2026年8月：内部开发的 Intern-S2 版本及其配套系统达到可用于深入数学探索的阶段。
- 9月29日：张杰松的论文发布于 arXiv，并于10月13日更新。
- 2026年10月15日：这一成果对外公布。
数学家如何引导人工智能
Intern-S2 首次探索这一问题时生成了一份约400页的推导报告。许笛声邀请自己的前学生、在瑞典皇家理工学院从事博士后研究的张杰松作为访问学者加入合作。张杰松自博士阶段起就一直关注吉斯猜想。
许笛声和张杰松审查模型提出的方案，找出有希望的切入点，并提供反馈以引导后续探索。机器探索不同的推理路径并生成论证；数学家则决定哪些方向值得继续研究，并协助完善最终证明。
实验室称，整个过程包括七轮持续推理。在此期间，模型的问题图从15个节点扩展到389个，累计输出约达千页，其中包括数十种拟议思路。
问题图是对较小数学任务及其相互关系的映射。一个节点可能代表某个中间结论，另一个节点则代表证明该结论所需的结果。据称节点数量的增长体现了系统对问题拆分和探索的广度。
张杰松在人工智能使用声明中直接说明了最终数学成果的责任归属：内部版本的 Intern-S2 通过多轮对话帮助发展思路和论证，而他独立核查了数学内容。他还在论文中感谢许笛声持续参与讨论。
配套软件发挥的作用
上海人工智能实验室为模型配备了软件，用于管理较长的推理链和反复的人类反馈。该系统能够将难题拆分为较小任务，探索多种方向，并将结果交由研究人员评估。
训练方法结合了广泛的科学知识与针对研究数学的材料，包括取自数学论文的难题，以及检查拟议解答的方法。实验室还介绍了采用可验证奖励的强化学习，也就是说，成功且可检查的推理能够提供训练信号。
研究人员随后利用配套系统积累的经验改进模型。实际目标是在长期研究中持续取得有用进展，包括跟踪中间结果，并在新论证逐步形成时纠正错误。
实验室还提到了 IMO-Proof 和 AdvancedMathBench 的结果，这两项评测侧重数学推理。对于吉斯猜想项目，关于系统如何运作的最详尽证据，是一系列深入推导、专家反馈、最终完成的论文以及后续的形式化验证。
北京大学团队如何核查证明
由董彬和刘若川领导的北京大学团队使用 SHEAF 框架，将张杰松论文中的四个主要定理全部形式化。相关工作还涵盖了论证所依据的吉斯研究成果。
形式化是将数学定义、假设和推理转化为计算机可检查的语言。传统论文可以依赖受过训练的读者补足熟悉的步骤；Lean 则要求通过精确的陈述和许可的逻辑操作，将这些步骤明确表达出来。
团队成员江杰东和吴斌表示，这项工作耗时约五天，最多有100个 AI 智能体并行运行，最终生成约55万行 Lean 代码。专家还核查了形式化陈述是否准确体现论文主要定理的数学含义。
SHEAF 将任务组织成一个由定义、命题及其依赖关系构成的有向图。这样，不同智能体可以处理彼此关联的部分，同时由团队跟踪哪些陈述已有证明、哪些仍待完成。
形式化工作不只是翻译最终论证。现有形式化数学库中缺少一些动力系统方面的辅助结果。团队必须补充这些基础，或寻找能够利用现有结果的路径，再将各部分串联成完整的证明链。
论文已作为预印本发布于 arXiv，形式化代码也已在 GitHub 上公开。公告未说明论文是否已发表于期刊，也未提及同行评审结果。
两个阶段为何缺一不可
Intern-S2 和 SHEAF 承担了不同任务。前者帮助寻找数学思路和论证，后者协助构建 Lean 可以检查的形式化证明。数学家负责引导探索、核查所得数学内容，并评估形式化陈述是否准确表达了预期定理。
工作规模具体体现了这种分工。约千页的探索性输出为研究论文提供了基础；随后，验证流程生成了约55万行形式化代码。每个阶段都将成果转化为适合不同任务的形式。
对于未来的研究人员，公开论文呈现了数学论证，公开代码则记录了形式化证明结构。形式化过程中补充的定义和结果，也可能为该领域今后的研究提供起点。
下一步是打造可复用的验证模块
上海人工智能实验室计划将这套工作流程封装为数学验证模块，供其 Intern Duanyan 科学发现平台使用。目标是让后续项目能够复用模型探索、专家反馈和形式化检查相结合的流程。
实验室还计划将这项项目中发展出的推理能力应用于具有相关数学结构的其他学科。设想中的循环是：解决一个研究问题，将有用的方法转化为可复用的软件，再将其应用于另一项研究。
对许笛声而言，这一成果通过大湾区大学、上海人工智能实验室、瑞典皇家理工学院和北京大学之间的合作，拓展了他长期关注的研究方向。对更广泛的数学界而言，它既带来了一项新的分类结果，也提供了人工智能在人类指导下参与研究的详细案例。
要点
- 这项新证明解决了吉斯猜想的余维一情形，包括复维数三的情形。
- 张杰松是研究论文的唯一作者，并表示自己独立核查了全部数学内容。
- 许笛声和张杰松通过反复探索和反馈引导 Intern-S2。
- 模型的问题图从15个节点扩展到389个，推导输出约达千页。
- 北京大学团队使用 SHEAF 框架，将四个主要定理及辅助结果形式化为 Lean 证明。
- 据称验证工作耗时约五天，生成约55万行代码。
- 实验室计划将这套工作流程转化为可复用的数学验证模块。
