近日，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之路。

联系我们

序号

负责内容

负责人及手机号

01

入会咨询&投稿&AI出海

王   健13058033327（aiiatrz@126.com）

02

场景打造&人形机器人租赁&AI新品推广

尚嘉俊13709577554

03

人工智能终端产品销售&发展经销商代理商

周   屏13168795405

04

OPC创业&投资孵化

王慧君13392892806

05

技能竞赛&技能认定

杨诗虹13826176348

06

校企合作&技能培训

张宇豪18475683370

07

品牌活动&国际交流

黄俊杰13392892803

08

公益培训&企业培训

何月岚19820812325

09

标准制定

白力伟19925280954

10

党建&工会&团委

王佳敏 18378704092

11

全国工商联人工智能委员会

吕   刚13392892810

12

RISC-V联盟广东省中心

黄子芹13144034109

13

展会展览

唐剑铭15818569461

14

检测认证

吕   刚13392892810

15

产业研究

徐   诺13693909813

16

供应商入库&政府招商

党军峰13480138058

非诚勿扰，请根据实际需求咨询相关工作人员

OCR:IMG:ANA

OCR:IMG:SAIR Events CompetitionsNEw Collaborations 国 N 鱼 Signin Overview Evaluation Setup Leaderboard My Submission My Team Solo Solo Marathon Marathon Gemma431BIT GPT-OSS120B Gemma431BIT GPT-OSS120B Main Leaderboard Research Leaderboard Published Sep 21. 2026.09:02 AM Evaluation configurationV Rank Team Score Solver size (KiB) Total Elapsed Details yanbiao.ai 福 200 EQT02-100037 478.798 4h 15m 17s Detalls

OCR:IMG:V ΛIIM 深圳市人工智能产业协会 enzhenArtificialIntelligenceIndustryAssociat AI服务人类美好世界 全国“四好”商会 广东省人工智能训练师职业技能等级认定 社会培训评价组织 深圳市AAAAA社会组织 深圳市两新组织先进基层党组织 深圳市高技能人才培养基地 深圳市技能成果交流展示基地 深圳市人工智能产业标准体系理论研究 深圳市质量基础设施”一站式“服务平台 深圳市人工智能产业协会知识产权工作站

OCR:IMG:DataCanvas 九章云极 人工智能基础设施及智算云提供商

OCR:IMG:ANA

OCR:IMG:(

OCR:IMG:V ΛII 深圳市人工智能产业协会 enzhenArtificialIntelligenceIndustryAssociat AI服务人类美好世界 全国“四好”商会 广东省人工智能训练师职业技能等级认定 社会培训评价组织 深圳市AAAAA社会组织 深圳市两新组织先进基层党组织 深圳市高技能人才培养基地 深圳市技能成果交流展示基地 深圳市人工智能产业标准体系理论研究 深圳市质量基础设施”一站式“服务平台 深圳市人工智能产业协会知识产权工作站 公众号·深圳市人工智能产业协会

OCR:IMG:arKiv QSe ComputerScience>LogicinComputerScience [Submitted on4Sep2026] agmas:Proof-Producing InfiniteCountermodelsand28NewOrder-FiveAustinClassifications 2g antusi constructor-tree carrier.The default product pairs its arguments;finitely many positive H ity of the exceptionalrelationby descent onconstructorsize,proves theidentity by exha titieswithno prior publicclassificationin our auditTheyform14 duality classes andesta th ations in94 canonical classes.Only Twee returns trusted counter-satisfiable outcomes,f e emit self-containedLean 4certificates Comments: 34 pages,2 figures,7 tables. Code and reproducibiity artifacts: this htps URL Subjects: Logic in Computer Science （cs.LO);Logic（math.LO) MSC classes classes:68v15 （Primary）08B05,03B35,03c05 （Secondary） ACM classes:F.4.1;I.2.3 Cite as: arXiv:2609.05690[cs.LO] （orarXiv:2609.05690v1[cs.LO]for this version） https://doi.org/10.48550/arXiv.2609.05690

OCR:IMG:理事会 动态