Jiuzhang Cloud's Yanbiao Lab Tops Terence Tao's Math Distillation Challenge with Reinforcement Learning for Lean 4 Proofs

让 AI 探索更广袤的未知。

编辑｜冷猫

2026 年 9 月 11 日，一封联名声明震动了学术界。

28 位菲尔兹奖得主联合署名发表了《人工智能在数学中的严重错位》，措辞罕见地尖锐。声明指出，AI 公司把解决数学难题当作衡量自身能力的 benchmark，这种做法「对数学科学和数学共同体是有害的」。

解题只是手段和代理指标，数学研究真正追求的是概念性的理解与洞察。当 AI 以越来越快的速度批量生产「对 / 错」判定，可能摧毁的恰恰是孕育新思想的沃土。

2026 年 9 月底，由陶哲轩联合创立的 SAIR Foundation 公布了数学蒸馏挑战赛（Mathematics Distillation Challenge）第二阶段的成绩。

在 294 支参赛队伍中，来自九章云极的言表实验室（yanbiao.ai）在全部四个赛道均取得满分 200 分，总榜得分高达 221 分，大幅领先其他参赛选手，为当之无愧的唯一头名。

陶哲轩一边参与批评 AI 公司用数学刷榜的做法，一边亲自组织了一场要求 AI 给出可验证证明的数学比赛。

他反对的从来都是「只追求答对、不关心理解」的路径，而非 AI 做数学本身。那么问题来了，什么样的 AI4S 策略，才能获得陶哲轩的认可？

一场「猜对不给分」的数学比赛

本次的第二阶段赛事聚焦等式理论中的蕴含关系，核心比赛规则为：

• 如果蕴含成立，参赛系统必须提交一份 Lean 4 形式化证明；
• 如果蕴含不成立，必须提交一个反例（一个满足前提但违反结论的代数结构）；
• 所有提交由确定性的 Lean 验证器逐一检验，验证未通过不得分。

换句话说，比赛的评判标准被从「答对率」改写成了「可验证性」。

比赛本身要求形式化验证，其实就已经表明了陶哲轩的立场。在他的设想中，关键是如何从大量数学证明中提炼出核心知识，并将其压缩进一个提示词。当这些高度浓缩的知识能够帮助模型解决新的数学问题时，知识便在某种意义上转化成了智能。让知识压缩成为智能提升的途径，正是他的愿景。

数学蒸馏挑战赛第二阶段赛事设有四个赛道，按两个维度交叉划分。

Solo 赛道每次处理一个问题，有固定的单题预算；Marathon 赛道则一次性处理 100 个问题，共享全局预算。两种模式考察的能力侧重不同，Solo 侧重单题攻坚深度，Marathon 侧重资源分配与整体策略。

在所有四个赛道中，九章云极的求解器均完成了全部评测题目，均以满分 200 分位列主榜第一。

主榜之外，比赛还设置了一个 Research Leaderboard（研究附加榜）。

根据赛事官方的评测框架，比赛评测集按难度分为 Normal、Hard、Extra Hard 和 Order 5 四个级别，其中 Order 5（五阶）等式涉及约 62000 条法则，涵盖了大量此前尚无定论的开放问题。Research Leaderboard 正是从这些五阶等式中筛选出最困难的部分，以此单独评分。

在所有参赛队伍中，仅有两支队伍得到了大于零的分数：九章云极以 17 分断崖式领先，第二名仅 3 分，其余全部为 0 分。

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

这次，28 个开放问题有了新答案

在比赛中，九章云极拿出了惊人的成果。这次，他们将在比赛中取得的新结果整理成了一篇论文，直指挑战赛中涉及 Austin 法则的难题。

• 论文标题：Trace-Tree Magmas: Proof-Producing Infinite Countermodels and 28 New Order-Five Austin Classifications
• 论文链接：https://arxiv.org/abs/2609.05690

什么是 Austin 法则？直觉上可以这样理解。在代数结构（magma，即一个集合配上一个二元运算）的世界里，大部分等式定律要么在有限结构中就能找到有趣的例子，要么根本不成立。但 Austin 法则不一样。它定义了这样一类特殊等式：所有满足它的有限代数结构都是平凡的（只有一个元素），但确实存在满足它的非平凡无限结构。

论文的核心贡献可以从三个层面理解。

第一，方法创新。 论文提出了「秩递减稀疏迹树 magma」（rank-decreasing sparse trace-tree magma）这一新构造。简单来说，团队设计了一种方法，用有限条重写规则，在无限的构造树上定义出一个真正无限的代数结构。这种「有限呈现无限」的思路，绕开了有限模型搜索器的根本局限。

第二，数学新发现。 在 ETP 锁定的 96 个五阶候选等式中，论文为其中 28 个此前没有任何公开分类的等式首次构造出非平凡无限模型，建立了 28 项新的 Austin 分类，归于 14 个对偶类。一次搜索共生成 636 份 Lean 4 证书，全部被赛事验证器接受。

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

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

诞生于智算云的冠军

在九章云极取得冠军成绩后，机器之心与九章云极 AI 首席科学家缪旭博士进行了深度的访谈交流。

这个组合乍看有些意外。AI 基础设施及智算云公司做数学推理比赛？但仔细想想，恰恰是合理的。

我们知道，AGI 的时代已经来临，RSI 是一个极其重要的课题。AI for Science 则是 RSI 率先落地的场景，而具备形式化验证能力的数学推理，则自然成为了第一站。缪旭在采访中回忆，「我们希望是一个开源的实体，大家作为一个社区，一起来解决问题。」SAIR 的开放理念与九章的方向高度一致，挑战赛成为了一个很好的切入口。

陶哲轩提出了「知识经过压缩就能转化为智能」的愿景，而九章云极则希望将这一思路进一步拓展。缪旭博士认为：「九章做 RSI，希望两边能够一起进化：不仅进化模型本身，也要进化人类的知识。」

而对九章云极来说，这场比赛还多了一层含义：以形式化验证为核心的 AI4S 负载，对算力底座的调度效率与长时稳定性提出了不同于以往的要求，这恰好是九章云极长期积累的方向。理念契合之外，这场挑战赛也成了一次工程能力的正面检验。

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

在挑战赛中断崖领先，对基础设施的需求是有壁垒的，而这恰巧是九章云极的传统强项。缪旭博士在采访中直接把这一点摆在了首位：「作为一家智算新云厂商，首先还是把底层基础设施做扎实。这里面确实有很多硬骨头要啃。」

他举了一个具体的例子，比赛中有些题目的 Lean 证明需要运行长达一个小时，团队对 Lean 系统做了大量优化，让系统加载更快、能够并行运行大量 Lean 进程，才把 RSI 实验的规模拉上去。

「通过打比赛、做科研项目，来试试看九章云极底层工程化能力是否能够支持这样的工作」，缪旭说，这本身就是参赛的目标之一。

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

「有时候，计算资源利用得比较高效，东西确实就能做得比较快。」这是一条朴素的真理。

可信任的 AI4S 能力

AI for Science 正在经历一个从「加速计算」到「参与发现」的范式转换。

在数学领域，模型已经能够跟数学家一起合作，能力早已经达到了研究级别。就在最近，OpenAI 宣布其 AI 系统产出了 722 个数学发现，引发广泛关注。然而数学家很快发现，部分结果存在错误或无法独立复核，几项成果甚至出现了符号错误，在审查后被撤回。

AI 的科研结论，到底能不能被信任？

2026 年科学智能大会（AI4S Congress）上，缪旭博士在 AI4S 基础理论平行会议的受邀报告中也谈到了这一点。他认为，AI4S 一大瓶颈是科研人员对 AI 推理结论的「信任赤字」。

大语言模型的概率性生成机制天然带来「幻觉」风险。在日常对话中，偶尔的事实偏差可以被容忍；在科学推理中，一个被遗漏的前提、一个被隐式替换的定义、一个在长推理链中积累的微小误差，都可能导致结论无效。

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

九章云极的应对路径是神经符号验证与强化学习闭环的结合，目标是让 AI 的每一次科学发现都具备可验证、可追溯的可靠性。RSI 这条路不应该完全是模型自己的迭代，「它很可能要跟形式化验证、跟知识库一起进化」。

数学天然具备形式化验证的能力，而在不久的未来，AI4S 系统一定会从数学领域起步，拓展到实验科学。

缪旭博士透露，在未来「我们希望把数学这套、以形式化验证为基础的系统，往其他实验性学科拓展。如果能跟实验性学科结合，我觉得才是真正有价值的事情，才真正能对人类科学进步起到很大作用。」

然而，从数学走向物理、化学、生物等实验科学，面临着一个最大的「信任赤字」瓶颈。这些领域缺少形式化验证体系。很多科学假设最终需要通过真实实验来验证，而实验往往耗时漫长、成本高昂。

即使是 AlphaFold 这样已经取得重大突破的 AI 系统，也无法完全跨越这道门槛。模型可以快速预测大量蛋白质结构，但真正进入实验环节，其中很多结果可能并不可行，仍然需要研究人员逐一筛选、验证。

九章云极希望从理论端寻找突破口。缪旭透露，团队的思路是构建物理、化学、材料等学科的形式化知识库，将相关理论体系逐步纳入可验证、可推理的系统。在真正开展实验之前，先通过理论推理排除明显不合理的假设，识别不同理论之间的矛盾，筛选更值得验证的研究方向。

AI 有机会成为连接两者的桥梁。 一方面，通过形式化推理和验证，让理论更直接地指导实验；另一方面，通过实验反馈，不断修正和丰富理论知识，进而推动 AI 系统的持续进化。

这是一项非常庞大的工作，如果这一循环能够建立起来，RSI 的价值也将从数学证明延伸到更广泛的科学发现过程。

通往更广泛科学的新基建

九章云极自身的 AI4S 布局，是一条持续延伸的科研脉络上的新节点。

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

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

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

从数学推理到智能体自进化，再到世界叙事模型、量子计算，九章云极的研究布局广泛，背后却有一条清晰的技术主线。

「主线实际上是围绕强化学习」，缪旭在采访中给出了明确的回答。

对于强化学习，缪旭还有一个更长远的设想：「我们希望形成一套比较通用的方法论，让这套方法论变成基础设施，再交给专业的人去完成专业的事情。」

这句话也点出了九章云极的理念：将强化学习沉淀为可复用的基础设施，为不同领域的专业研究提供支撑。 随着 AI for Science 从数学走向更广泛的实验科学，这套基础设施也有望成为推动 AI 深度参与科学研究的重要底座。

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

在采访的末尾，缪旭博士提到了一个让他印象深刻的场景。参加 AI Congress 之后，有人跟他说，很多年轻数学家觉得自己的行业要被 AI 颠覆了，感到沮丧。

「但我不这么觉得」，缪旭说，「AI 应该帮助人发现更多未知，而不是把我们所有已知的氧气全部吸走，让我们没有氧气可以呼吸。」

人认知的东西越多，未知的也会越多。「如果只是抢现有的存量问题，人是抢不过机器的，迟早会被替代。但如果有增量，那就是一个非常大的世界变化。」

这句话让人想起陶哲轩发起这场比赛的初衷：他要的从来都是 AI 帮助数学家理解更多、发现更多，而非替代数学本身。

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

© THE END

转载请联系本公众号获得授权

投稿或寻求报道：[email protected]