编辑｜冷猫 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 个五阶候选等式中，论