九章云极问鼎陶哲轩数学挑战赛！让强化学习成为AI4S新基建
2026.10.13 · 事件 · AI 事件 · 媒体报道
九章云极言表实验室在数学蒸馏挑战赛四赛道满分夺冠，并首次给出28个五阶等式的新分类。
九章云极旗下言表实验室在陶哲轩联合创立的 SAIR 数学蒸馏挑战赛第二阶段中，四个赛道均以满分 200 分位列主榜第一，研究附加榜以 17 分断崖领先。团队将成果整理为论文，为 28 个此前无公开分类的五阶等式首次构造非平凡无限模型，生成 636 份 Lean 4 证书全部通过验证。
- 四赛道均满分 200 分，主榜唯一头名
- 研究附加榜 17 分，第二名仅 3 分
- 论文首次建立 28 项新 Austin 分类
- 一次搜索生成 636 份 Lean 4 证书
- 证明图压缩至 500 KB Python 代码
为什么值得看
看形式化验证如何把数学推理变成可信任的 AI4S 基建。
适合谁关注
关注 AI4S、强化学习与形式化验证的从业者。