文章摘要
2026年9月，陶哲轩联合创立的SAIR Foundation公布数学蒸馏挑战赛第二阶段结果，九章云极旗下言表实验室团队斩获头名，四个赛道全满分，附加榜大幅领先。该团队提出新构造方法，为28个尚无公开分类的开放数学问题完成新分类，所有成果均通过形式化验证，依托全栈智算能力推进可验证AI赋能科学研究。

2026年9月，学术界迎来一则震动性的联名声明：28位菲尔兹奖得主联合发表文章，尖锐批评部分AI企业将解决数学难题作为自身能力的衡量基准，认为这种做法对数学科学与共同体有害。声明指出，解题只是手段而非目的，数学研究真正追求的是概念性的理解与洞察，而批量生产对错判定的AI模式，反而可能摧毁孕育新思想的沃土。

就在同一月，由陶哲轩联合创立的SAIR Foundation公布了数学蒸馏挑战赛第二阶段的赛事结果。有趣的是，陶哲轩一边参与批评AI刷榜的短视做法，一边亲自组织了这场要求AI提供可验证证明的数学竞赛——他反对的从来不是AI参与数学研究，而是只追求答对答案却不关心底层理解的路径。

在294支参赛队伍中，来自言表实验室的参赛团队表现惊艳，在全部四个赛道均取得满分200分，总榜得分高达221分，大幅领先其他选手，成为当之无愧的头名。

一场零容错的竞赛规则

本次赛事第二阶段聚焦等式理论中的蕴含关系，核心评判标准完全抛弃了传统的答对率，转而以可验证性作为核心指标，具体规则包括：

  • 当蕴含关系成立时，参赛系统需要提交一份Lean 4形式化证明，确保每一步逻辑都严谨可追溯

  • 若蕴含不成立，则必须提供一个反例，即满足前提但违背结论的代数结构

  • 所有提交内容都会经过确定性的Lean验证器逐一校验，未通过验证的提交将无法获得分数

赛事按两个维度交叉设置了四个赛道：Solo赛道每次处理单个问题，配有固定单题预算，侧重单题攻坚的深度；Marathon赛道则一次性处理100个问题，共享全局预算，更考察资源分配与整体策略能力。

除了主榜单外，赛事还设置了研究附加榜，从难度最高的Order 5（五阶）等式中筛选最困难的题目单独评分。五阶等式涉及约62000条法则，涵盖大量此前尚无定论的开放问题。在该榜单中，仅有两支队伍获得了大于零的分数，参赛团队以17分断崖式领先，第二名仅得3分，其余队伍均为0分。

值得一提的是，参赛团队在多个赛道中使用了同一套智能体与方法。在迭代过程中，团队构建了包含数十亿条Lean代码的证明图，并将其压缩到比赛要求的500KB Python代码中，无需分别设计多个智能体和算法工具。

28个开放问题的全新突破

本次赛事中，参赛团队将研究成果整理成了学术论文，直指挑战赛中涉及Austin法则的核心难题。Austin法则定义了一类特殊的代数等式：所有满足该等式的有限代数结构都是平凡的（仅包含一个元素），但确实存在满足该等式的非平凡无限结构。

这篇论文的核心贡献可以从三个层面展开：

  • 方法创新：提出了「秩递减稀疏迹树magma」的新构造，通过有限条重写规则在无限构造树上定义出真正的无限代数结构，绕开了有限模型搜索器的根本局限

  • 数学新发现：在ETP锁定的96个五阶候选等式中，首次为其中28个此前无公开分类的等式构造出非平凡无限模型，建立了28项新的Austin分类，归于14个对偶类，共生成636份Lean 4证书并全部通过赛事验证器校验

  • 可验证性贯穿始终：每一个报告的模型都附带一份自包含的Lean 4证明，团队将这套机制称为「信任边界」设计，搜索与生成程序本身不被信任，所有候选结果必须通过Lean内核验收才会被计数

论文的主要贡献者来自言表实验室，该实验室是所属的AI4S研究机构，而本身是一家人工智能基础设施及智算云提供商。

论文标题为《Trace-Tree Magmas: Proof-Producing Infinite Countermodels and 28 New Order-Five Austin Classifications》，相关成果可通过arxiv链接https://arxiv.org/abs/2609.05690查阅。

智算底座支撑的夺冠底气

作为一家智算云厂商，能在数学推理赛事中取得领先成绩看似意外，实则合理。AI for Science是强化学习率先落地的场景，而具备形式化验证能力的数学推理正是其中的核心方向。

在采访中，相关负责人回忆，团队希望打造一个开源社区，共同推动问题解决，而赛事的开放理念与公司的方向高度契合，成为了很好的切入场景。陶哲轩提出「知识经过压缩就能转化为智能」的愿景，而团队希望将这一思路进一步拓展，不仅进化模型本身，也要进化人类的知识。

对来说，这场赛事也是一次工程能力的全面检验。以形式化验证为核心的AI4S负载，对算力底座的调度效率与长期稳定性提出了不同于以往的要求，而这正是长期积累的优势领域。

自动数学推理属于特殊的计算负载，求解器需要在「搜索证明→形式化验证→根据反馈调整策略」的循环中持续迭代，涉及大规模并行搜索、长时间运行和高效资源调度，与强化学习训练面临的工程挑战高度相似。

相关负责人表示，作为智算厂商，首先要把底层基础设施做扎实，团队为此做了大量优化：比如针对部分题目Lean证明需要运行长达一小时的情况，对Lean系统进行了大量优化，提升加载速度并支持并行运行大量Lean进程，才得以扩大RSI实验的规模。通过这场赛事，团队也验证了底层工程化能力能否支撑这类新型工作负载。

围绕九章智算云与智算操作系统，构建了从硬件适配、算力调度到模型训练与智能服务交付的全栈能力。训练工厂支持异构算力上的大规模预训练、微调与强化学习负载，Token工厂则承载高吞吐推理任务，二者构成从训练到落地的完整工程底座。持有超过29000PFLOPS的可控算力，率先提出DCU（一度算力）度量单位，推动算力像水电一样可计量、可结算，相关实践入选工业和信息化部2025年度新型信息基础设施典型案例。

相关负责人用朴素的真理总结了这一点：计算资源利用效率更高，研发推进的速度也会更快。

破解AI4S的信任赤字难题

AI for Science正在经历从「加速计算」到「参与发现」的范式转换，当前AI系统已经能够与数学家展开合作，甚至达到研究级别的能力。但近期相关AI产品宣布产出大量数学发现后，部分结果被发现存在错误或无法独立复核，甚至出现符号错误并被撤回，引发了关于AI科研结论可信度的广泛讨论。

在2026年科学智能大会上，相关负责人指出，AI4S面临的一大瓶颈是科研人员对AI推理结论的信任赤字。大语言模型的概率性生成机制天然带有「幻觉」风险，在日常对话中偶尔的事实偏差尚可容忍，但在科学推理中，一个遗漏的前提、隐式替换的定义或是长推理链中积累的微小误差，都可能导致结论完全无效。

2026年3月发布的《人工智能安全治理框架》2.0版，也将模型输出的可靠性与可验证性纳入治理体系，明确要求在高风险决策场景中强化可追溯、可审计的技术能力，这意味着AI赋能科研不仅要算得快，更要算得可信。

的应对路径是结合神经符号验证与强化学习闭环，目标是让AI的每一次科学发现都具备可验证、可追溯的可靠性。团队认为，强化学习的发展路径不应该仅依赖模型自身迭代，而是需要与形式化验证、知识库共同进化。

数学天然具备形式化验证的基础，而AI4S系统也将从数学领域起步，逐步拓展到实验科学领域。相关负责人透露，团队希望将数学领域以形式化验证为基础的系统，拓展到物理、化学、材料等实验性学科，通过构建各学科的形式化知识库，将相关理论体系逐步纳入可验证、可推理的系统。在真正开展实验之前，先通过理论推理排除明显不合理的假设，识别不同理论之间的矛盾，筛选更值得验证的研究方向。

AI有机会成为连接理论与实验的桥梁：一方面通过形式化推理和验证，让理论更直接地指导实验；另一方面通过实验反馈，不断修正和丰富理论知识，推动AI系统持续进化。如果这一循环能够建立起来，强化学习的价值也将从数学证明延伸到更广泛的科学发现过程。

迈向跨学科科学的新基建布局

的AI4S布局是一条持续延伸的科研脉络上的新节点。与北京大学的深度合作是这条脉络的重要一环：双方共建「北大 - 多智能体联合实验室」，重点布局Agentic RL方向，四大研究方向中的「数学智能体与复杂推理」直接关联本次赛事和论文成果。实验室实现了「科研有算力、算法有场景、成果有落地」的双向协同，北大提供原创算法思想与高端科研人才，开放万P级异构算力集群、全栈智算云以及金融、制造、科研等真实产业场景。

前沿研究的参与深度也在不断加码：作为核心算力支持方与生态共建伙伴，深度参与上海交通大学张文军院士团队「世界叙事模型」的研发攻关，为复杂的多模态训练与物理仿真推演提供高性能算力底座，相关负责人深度参与论文编写与课题攻关，从算力供应延伸到了技术共创。

还在AIGC评测方向建设了多维度的评测智能体系统，相关项目获认可并加入国家重点实验室共建名单。此外，团队还完成了与玻色量子Kaiwu SDK的适配验证，AI工厂打通量超融合技术链路，展示了多智能体强化学习框架在量子计算方向的工程实践能力。

从数学推理到智能体自进化，再到世界叙事模型、量子计算，的研究布局广泛，但背后有一条清晰的技术主线。相关负责人明确表示，这条主线实际上是围绕强化学习展开的。

对于强化学习，团队还有更长远的设想：希望形成一套通用的方法论，将其沉淀为可复用的基础设施，交给不同领域的专业人员使用。随着AI for Science从数学走向更广泛的实验科学，这套基础设施也有望成为推动AI深度参与科学研究的重要底座。

尾声：让AI探寻更广袤的未知

在采访的末尾，相关负责人提到了一个印象深刻的场景：在科学智能大会后，不少年轻数学家表示担心自己的行业会被AI颠覆，感到沮丧。但他并不这么认为：「AI应该帮助人发现更多未知，而不是把我们所有已知的氧气全部吸走，让我们没有氧气可以呼吸。」

人类认知的边界越拓展，未知的领域也越多。如果只是争夺现有的存量问题，人类终究会被机器替代；但如果聚焦于增量的未知领域，这将是一个无比广阔的世界。这也恰好呼应了陶哲轩发起这场赛事的初衷：他要的从来不是AI替代数学研究，而是帮助数学家理解更多、发现更多。

好的AI for Science，应该带领人类探索更广袤的未知。正在这条路上继续前进。

以上内容不代表本平台立场，仅供读者参考