九章云极问鼎陶哲轩数学挑战赛，四个赛道均获满分

2026年9月11日，28位菲尔兹奖得主联合署名发表《人工智能在数学中的严重错位》，指出AI公司把解决数学难题当作衡量自身能力的benchmark“对数学科学和数学共同体是有害的”。这份声明的逻辑是：解题只是手段和代理指标，数学研究真正追求的是概念性的理解与洞察。

半个月后，2026年9月底，由陶哲轩联合创立的SAIR Foundation公布了数学蒸馏挑战赛第二阶段的成绩。表面上看，这是一场AI做数学的比赛，与那份声明的批评对象似乎重合；但比赛规则本身给出了另一种回答：如果蕴含成立，参赛系统必须提交一份Lean 4形式化证明；如果蕴含不成立，必须提交一个反例，即一个满足前提但违反结论的代数结构；所有提交由确定性的Lean验证器逐一检验，验证未通过不得分。

换句话说，评判标准被从“答对率”改写成了“可验证性”。这是理解整件事的枢纽：陶哲轩反对的从来是“只追求答对、不关心理解”的路径，而非AI做数学本身。比赛要求形式化验证，本身就是一种立场表达。

在294支参赛队伍中，来自九章云极的言表实验室（yanbiao.ai）在全部四个赛道均取得满分200分，总榜得分221分，大幅领先其他参赛选手，位列唯一头名。四个赛道按两个维度交叉划分：Solo赛道每次处理一个问题、有固定的单题预算，侧重单题攻坚深度；Marathon赛道一次性处理100个问题、共享全局预算，侧重资源分配与整体策略。

更能说明难度分布的是主榜之外的Research Leaderboard（研究附加榜）。赛事评测集按难度分为Normal、Hard、Extra Hard和Order 5四个级别，其中Order 5（五阶）等式涉及约62000条法则，涵盖大量此前尚无定论的开放问题。研究附加榜正是从这些五阶等式中筛选出最困难的部分单独评分。在所有参赛队伍中，仅有两支队伍得分大于零：九章云极以17分领先，第二名仅3分，其余全部为0分。

值得注意的是，在多个赛道中，参赛团队均使用同一套智能体和方法。团队在迭代过程中发现不需要分别设计智能体和算法工具，而是构建了一个包含数十亿条Lean代码的证明图，再将其压缩到比赛要求的500 KB Python代码以内。这一点是工程约束，也是方法选择：它意味着成绩并非来自针对不同赛道的定制化调参。