九章云极问鼎SAIR数学蒸馏挑战赛 四赛道满分全球第一

近日，SAIR Foundation 数学蒸馏挑战赛（Mathematics Distillation Challenge）第二阶段公布主榜成绩。九章云极言表实验室（yanbiao.ai）参赛团队在全部四个赛道均取得满分第一，进入全球主榜满分阵营。同期，九章云极与北京大学计算机学院联合完成的论文《Trace-Tree Magmas: Proof-Producing Infinite Countermodels and 28 New Order-Five Austin Classifications》公开发表（arXiv:2609.05690），首次为28个长期开放的数学等式建立新的 Austin 分类。

据了解，本次挑战赛由 SAIR Foundation 发起，菲尔兹奖得主、加州大学洛杉矶分校（UCLA）教授、SAIR Foundation联合创始人Terence Tao（陶哲轩），以及宾夕法尼亚大学统计学与数据科学副教授Damek Davis共同组织。言表实验室（yanbiao.ai）作为九章云极旗下的AI4S研究机构，聚焦自动推理、形式化验证与科学发现等场景。

一场不一样的数学比赛：“蒸馏压缩”是智能的来源

这项赛事为何叫“蒸馏”？参赛者的目标不是让 AI 生成更长、更复杂的推理，而是把机器产生的大量推演结果，压缩成泛化能力更强的证明文本，学界认为压缩是知识变成智能的原因，也是期待通过蒸馏压缩看到更强大的智能体。

本阶段比赛聚焦等式理论中的推理问题：给定两个等式，判断前者是否必然推出后者。参赛系统不能只回答“是”或“否”——蕴含成立时提交 Lean 4 形式化证明，不成立时提交反例，所有结果由确定性的 Lean 验证器逐一检验，验证未通过不得分。

这一机制把评判标准从“答对率”改写为“可验证性”：猜对不算数，证明通过才算数。在数学推理领域，这被视为衡量系统真实推理能力的硬标准。在这一机制下，言表实验室的求解器完成了全部赛道的所有评测题，以满分位列主榜并列第一。

从“会解题”到“能发现”：28 个开放问题首次有了答案

比赛证明的是“会解题”，论文展示的则是更难的能力——“能发现”。

这项由九章云极与北京大学计算机学院合作完成的研究，瞄准等式理论中的公认难题 Austin 法则：这类等式的所有有限模型都是平凡的，却存在非平凡的无限模型——没有哪张有限的乘法表，能够见证一个无限的存在，传统有限模型搜索器在原理上就无法触及。

论文的主要贡献者来自北大-九章云极多智能体联合实验室。该实验室由北京大学计算机学院杨仝教授与九章云极AI首席科学家缪旭博士共同领导，聚焦多智能体自进化能力研究。

团队的方法另辟蹊径：用有限条规则，在无限的构造树上“有限呈现”一个真正无限的数学结构；每一个被报告的模型，都必须附带一份自包含的 Lean 4 证明：

· 在国际等式理论项目（ETP）锁定的 96 个五阶候选等式中，为其中 28 个此前没有任何公开分类的等式首次构造出非平凡无限模型，建立 28 项新的 Austin 分类，归于 14 个对偶类；

· 一次完整搜索共生成 636 份 Lean 4 证书，全部被赛事验证器接受；

· 与国际主流自动定理证明器 Vampire等同资源对比中，三者对这 28 个等式无一能够判定，也无一能产出模型或形式化证书；

· 经系统的文献与公开成果审计，这是全球首个能够合成此类模型、生成其良基证明并输出自包含 Lean 4 证书的自动化系统。

支撑这些成果的，是一套“信任边界”设计：搜索与生成程序本身不被信任，任何候选结果必须通过 Lean 内核验收才会被计数。这与比赛的评测哲学一脉相承，也正是团队能在“满分”与“新发现”两条战线上同时成立的原因。

从工程底座到AI4S：算力与可验证性的交汇

自动数学推理对 AI 提出的要求，恰是推理能力与强化学习的交叉点：推理侧要求长链条逻辑推导保持稳定一致；强化学习侧则要在“证明搜索—验证反馈”的循环中持续优化策略。九章云极的求解器正是运行在这一交叉点上的一类特殊负载——大规模并行搜索、长周期迭代、集群持续高压下的稳定，这些需求与强化学习负载高度同构。这与九章云极的智算布局同向。训练工厂支持异构算力上的大规模预训练、微调与强化学习，Token 工厂承载高吞吐推理任务，二者构成从训练到落地的完整工程底座。从行业趋势看，强化学习正成为智算需求的第三曲线，此次的科研成果，正是这条曲线在科学问题上的一个切面。

而这次突破并非孤立的参赛获奖，而是九章云极科研脉络上的新节点：从早年团队在 Kaggle 登顶世界第一，到此次与北京大学计算机学院合作向基础研究延伸，九章云极在AI4S上的投入始终围绕一个交汇点——向下，以自研智算云平台提供可调度、可计量的算力底座；向上，让智能具备进入科学场景的可信资质。

AI4S的真正含义，不止于“算力+推理”的简单叠加。科学结论必须经得起复核：每一步推导可被独立验证，AI才能从“工具”走向“科研参与者”。算力决定AI能算多快，可验证性决定AI能走多远——九章云极给出的答案是两者都要：以自研智算云底座支撑“算得动”，以对可验证性的坚持保证“走得远”。这条既需要算力、又需要信任的路，正是九章云极选择的AI4S之路。