九章云极在陶哲轩数学蒸馏挑战赛四赛道满分居首
九章云极用「证明图压缩 + Lean 4 形式化验证」的强化学习路线拿下陶哲轩数学挑战赛四赛道满分，并首次完成 28 项 Austin 分类
陶哲轩联合创立的 SAIR 基金会举办数学蒸馏挑战赛第二阶段：AI 必须提交 Lean 4（可被机器逐条检验的证明语言）形式化证明或反例，「猜对」不给分。九章云极言表实验室四个赛道全部满分 200 分，研究附加榜以 17 分领先第二名 3 分。
正文摘录
.jpg) 编辑｜冷猫 2026 年 9 月 11 日，一封联名声明震动了学术界。 28 位菲尔兹奖得主联合署名发表了《人工智能在数学中的严重错位》，措辞罕见地尖锐。声明指出，AI 公司把解决数学难题当作衡量自身能力的 benchmark，这种做法「对数学科学和数学共同体是有害的」。 解题只是手段和代理指标，数学研究真正追求的是概念性的理解与洞察。当 AI 以越来越快的速度批量生产「对 / 错」判定，可能摧毁的恰恰是孕育新思想的沃土。 2026 年 9 月底，由陶哲轩联合创立的 SAIR Foundation 公布了数学蒸馏挑战赛（Mathematics Distillation Challenge）第二阶段的成绩。  在 294 支参赛队伍中，来自九章云极的言表实验室（yanbiao.ai）在全部四个赛道均取得满分 200 分，总榜得分高达 221 分，大幅领先其他参赛选手，为当之无愧的唯一头名。