九章云极包揽陶哲轩数学蒸馏挑战赛四赛道满分，解决 28 个开放问题
机器之心 · wechat · 2026-10-13
陶哲轩联合创立的 SAIR Foundation 公布数学蒸馏挑战赛第二阶段成绩：294 支队伍中，九章云极言表实验室（yanbiao.ai）在全部四个赛道均以满分 200 分登顶，总榜 221 分大幅领先。比赛要求蕴含关系成立必须提交 Lean4 形式化证明、不成立必须提交反例，评判标准是「可验证性」而非答对率。
团队还发布论文，提出「秩递减稀疏迹树 magma」构造，为 28 个此前无公开分类的五阶 Austin 等式首次建立非平凡无限模型，生成 636 份 Lean4 证书全部通过验证。研究附加榜上九章云极以 17 分断崖领先（第二名仅 3 分）。机器之心专访 AI 首席科学家缪旭：团队构建数十亿条 Lean 代码的证明图并压缩进 500KB 代码，靠大规模并行搜索与算力调度优势取胜，未来计划把形式化验证体系从数学拓展到物理、化学等实验科学。
「研究」频道最新
- 词向量减法新玩法：cartoon−animation−comic 减出 diagram — mayfer · 2026-10-23
- Omnii Genome 单一通用模型全面超越 AlphaGenome — JosephJacks_ · 2026-10-23
- Domingos 引新研究断言「强化学习基本没用」，引监督学习对比 — pmddomingos · 2026-10-23
- 实测「bathroom − toilet = kitchen」：embedding 算术优于稀疏自编码器 — mayfer · 2026-10-23
- Wolfram 宣布 Rule 30 三道悬赏题向 AI 开放，总奖金 3 万美元 — cephaloform · 2026-10-23
- 斯坦福联手 Databricks:用 AI Agent 复现医学论文结论并做稳健性检验 — ChengleiSi · 2026-10-23