如果一场数学比赛规定：猜对答案不给分，只认机器能逐行检验的证明，会发生什么？
2026年9月底，由陶哲轩联合创立的SAIR Foundation公布了数学蒸馏挑战赛第二阶段的成绩。294支参赛队伍里，来自九章云极的言表实验室在全部四个赛道均取得满分200分，总榜得分221分，位列第一。
更值得琢磨的是另一个榜单。主榜之外，赛事还设置了Research Leaderboard，从五阶等式中筛选出最困难的部分单独评分。所有参赛队伍中，仅有两支得分大于零：九章云极17分，第二名3分，其余全部为0分。
一场「猜对不给分」的比赛
这次第二阶段赛事聚焦等式理论中的蕴含关系，规则被改写得相当硬核：如果蕴含成立，参赛系统必须提交一份Lean 4形式化证明；如果蕴含不成立，必须提交一个反例，也就是一个满足前提但违反结论的代数结构。
所有提交由确定性的Lean验证器逐一检验，验证未通过不得分。评判标准从「答对率」变成了「可验证性」。
比赛设有四个赛道，按两个维度交叉划分。Solo赛道每次处理一个问题，有固定的单题预算；Marathon赛道一次性处理100个问题，共享全局预算。前者侧重单题攻坚深度，后者侧重资源分配与整体策略。九章云极的求解器在四个赛道中均完成了全部评测题目，均以满分200分位列主榜第一。
值得一提的是，在多个赛道中，参赛团队使用的是同一套智能体和方法。团队构建了一个包含数十亿条Lean代码的证明图，再将其压缩到比赛要求的500 KB Python代码中。
28个开放问题有了新答案
比赛之外，九章云极把取得的新结果整理成了一篇论文，直指挑战赛中涉及Austin法则的难题。
Austin法则的特殊之处在于：所有满足它的有限代数结构都是平凡的，只有一个元素，但确实存在满足它的非平凡无限结构。这恰恰是有限模型搜索器的盲区。
论文提出了「秩递减稀疏迹树magma」这一新构造，用有限条重写规则，在无限的构造树上定义出一个真正无限的代数结构，绕开了有限搜索的根本局限。
在ETP锁定的96个五阶候选等式中，论文为其中28个此前没有任何公开分类的等式首次构造出非平凡无限模型，建立了28项新的Austin分类，归于14个对偶类。一次搜索共生成636份Lean 4证书，全部被赛事验证器接受。
每一个被报告的模型，都附带一份自包含的Lean 4证明。团队把这套机制称为「信任边界」设计：搜索与生成程序本身不被信任，任何候选结果必须通过Lean内核验收才会被计数。
冠军背后的算力账本
九章云极是一家人工智能基础设施及智算云提供商，言表实验室是其旗下的AI4S研究机构。一家智算云公司拿下数学推理比赛的头名，这个组合乍看有些意外。
九章云极AI首席科学家缪旭在访谈中把底层基础设施摆在了首位：「作为一家智算新云厂商，首先还是把底层基础设施做扎实。这里面确实有很多硬骨头要啃。」
他举了一个具体的例子：比赛中有些题目的Lean证明需要运行长达一个小时，团队对Lean系统做了大量优化，让系统加载更快、能够并行运行大量Lean进程，才把RSI实验的规模拉上去。
自动数学推理在计算层面是一类非常特殊的负载。求解器需要在「搜索证明、形式化验证、根据反馈调整策略」的循环中持续迭代，涉及大规模并行搜索、长时间运行和高效资源调度，与强化学习训练面临的工程挑战高度相似。
九章云极围绕九章智算云与智算操作系统，构建了从硬件适配、算力调度到模型训练与智能服务交付的全栈能力。训练工厂支持异构算力上的大规模预训练、微调与强化学习负载，Token工厂则承载高吞吐推理任务。公司持有超过29000PFLOPS的可控算力，并率先提出DCU（一度算力）度量单位，推动算力像水电一样可计量、可结算，该实践入选工业和信息化部2025年度新型信息基础设施典型案例。
缪旭的说法很朴素：「有时候，计算资源利用得比较高效，东西确实就能做得比较快。」
信任赤字，才是真瓶颈
AI for Science正在经历一个从「加速计算」到「参与发现」的范式转换。在数学领域，模型已经能够跟数学家一起合作，能力达到了研究级别。
但另一面同样真实。OpenAI宣布其AI系统产出了722个数学发现，数学家很快发现部分结果存在错误或无法独立复核，几项成果甚至出现符号错误，在审查后被撤回。
缪旭在2026年科学智能大会的受邀报告中谈到了这一点。他认为，AI4S的一大瓶颈是科研人员对AI推理结论的「信任赤字」。大语言模型的概率性生成机制天然带来「幻觉」风险：在日常对话中，偶尔的事实偏差可以被容忍；在科学推理中，一个被遗漏的前提、一个被隐式替换的定义、一个在长推理链中积累的微小误差，都可能导致结论无效。
政策信号也在同步收紧。2026年3月发布的《人工智能安全治理框架》2.0版，将模型输出的可靠性与可验证性纳入治理体系，明确要求在高风险决策场景中强化「可追溯、可审计」的技术能力。
九章云极的应对路径是神经符号验证与强化学习闭环的结合，目标是让AI的每一次科学发现都具备可验证、可追溯的可靠性。缪旭的判断是，RSI这条路不应该完全是模型自己的迭代，「它很可能要跟形式化验证、跟知识库一起进化」。
从数学走向实验科学
数学天然具备形式化验证的能力。缪旭透露，未来「我们希望把数学这套、以形式化验证为基础的系统，往其他实验性学科拓展。如果能跟实验性学科结合，我觉得才是真正有价值的事情」。
难点在于，物理、化学、生物等实验科学缺少形式化验证体系。很多科学假设最终需要通过真实实验来验证，而实验往往耗时漫长、成本高昂。即使是AlphaFold这样已经取得重大突破的AI系统，也无法完全跨越这道门槛：模型可以快速预测大量蛋白质结构，但真正进入实验环节，其中很多结果可能并不可行，仍然需要研究人员逐一筛选、验证。
九章云极希望从理论端寻找突破口。团队的思路是构建物理、化学、材料等学科的形式化知识库，将相关理论体系逐步纳入可验证、可推理的系统。在真正开展实验之前，先通过理论推理排除明显不合理的假设，识别不同理论之间的矛盾，筛选更值得验证的研究方向。
这条脉络上还有几个节点：与北京大学共建「北大-九章云极多智能体联合实验室」，重点布局Agentic RL方向，四大研究方向中「数学智能体与复杂推理」直接关联本次赛事和论文成果；作为核心算力支持方与生态共建伙伴，深度参与上海交通大学张文军院士团队「世界叙事模型」的研发攻关；在AIGC评测方向建设多维度评测智能体系统；完成与玻色量子Kaiwu SDK的适配验证，打通量超融合技术链路。
布局看起来分散，缪旭给出的主线很明确：「主线实际上是围绕强化学习。」他还有一个更长远的设想：「我们希望形成一套比较通用的方法论，让这套方法论变成基础设施，再交给专业的人去完成专业的事情。」
尾声
采访末尾，缪旭提到一个让他印象深刻的场景。参加AI Congress之后，有人跟他说，很多年轻数学家觉得自己的行业要被AI颠覆了，感到沮丧。
「但我不这么觉得」，缪旭说，「AI应该帮助人发现更多未知，而不是把我们所有已知的氧气全部吸走，让我们没有氧气可以呼吸。」
人认知的东西越多，未知的也会越多。「如果只是抢现有的存量问题，人是抢不过机器的，迟早会被替代。但如果有增量，那就是一个非常大的世界变化。」
热门跟贴