The Problem Is the Problem: Towards Scalable Mathematical Discovery
Zeyu Zheng, Shengtong Zhang, Jeremy Avigad, Prasad Tetali, Sean Welleck
cs.AI, math.CO
2026-08-18
CMU 团队把 AI 做数学的接口从「人选一道题」改成「人给一个方向」,管线从 5245 篇组合数学论文中筛出 4717 个公开猜想,自动尝试后经多重过滤得到 77 项可发表结果,人工复核的 15 项全部数学正确。
AI 做数学的现有工作流,几乎都是人先选定一道题,再把模型放上去解。瓶颈正在转移:前沿模型的推理能力按预算买得到,而选对题、以及审读模型产出的数学证明,都依赖稀少的领域专家。人卡在管线的两头,中间的模型算力反而是最不稀缺的一环。
CMU 的这组作者(含 Lean 社区的 Sean Welleck 和数学家 Jeremy Avigad、Prasad Tetali)把接口改了:人不再指定具体问题,只给一个研究方向,比如「组合数学」。系统自己去文献里找值得做的题、去尝试、再把最值得人看的东西推到专家面前。从选一道题,变成选一个方向。
管线叫 FAR,即 Find(找)、Attempt(试)、Recommend(荐)三级级联,思路借自搜索与推荐系统:便宜的模型粗筛海量候选,贵的模型只处理漏斗末端越来越难、越来越少的部分。
一个关键设计是难度分 d 和重要性分 i 在检查阶段就打好(各以「不可发表的练习题 / 顶刊可发表」和「无内容 / Fields Medal 级」为 0 和 1 锚点),在任何推理预算花掉之前固定,事后就能拿实际产出验证这两个分数是否有效。
级联各层的数量:51,110 篇 → 5,245 篇 → 6,453 条候选 → 4,717 条公开猜想 → 1,050 条声称解答 → 598 条过审 → 77 条值得发表。4,717 次尝试中 2,905 次无结果,443 次发现文献已有答案,319 次发现题目本身有缺陷。
作者人工复核了 77 条中感兴趣的 15 条,未发现任何数学错误。代表性结果:
| 对象 | 类型 | 结果 |
| Davies-Jenssen-Perkins-Roberts 猜想(无三角形图的独立数比) | 反例 | C₅□K{m,m} 使比值趋于 24/13 < 2,换 C₁₃(1,5) 降到 32/19 |
| Erdős-Straus 二项式系数整除问题 | 解答 | 对每个固定 n ≥ 2,密度 d(n) = 1 |
| Ikenmeyer-Pak-Panova 对称群特征标猜想 | 证明 | 二行划分下 many-one 归约 GapP 完全性成立 |
| Lund-Saraf-Wolf 猜想(F₃q 中线的并集) | 反例 | 椭圆抛物面的半切线族给出密度 1/2+o(1) 的反例,对 q ≤ 13 穷举验证 |
难度分的 AUC 为 0.69(p < 10⁻⁴⁰),重要性分为 0.60(p = 0.008),两个分数与实际产出显著相关。预算分配实验里,按「可发表概率估计」排序在所有预算下都优于均匀随机基线;要最大化单一最重要成果时,只保留重要性前 1/10 再排序效果最好。
这篇把 AI-for-math 的稀缺资源从「模型能力」挪到了「专家注意力」上。77 比 4,717 的压缩比意味着数学家看到的每一条都过了模型自证、正确性裁判、价值分级三道闸,审读成本降了一个量级以上。对做 AI 研究基础设施的人,这是把推荐系统的漏斗思路搬进科研流程的一个完整落地样本:分级用便宜模型、攻坚用贵模型、预算分配有理论保证(部分目标可精确求解或 1-1/e 近似)。反例类的发现尤其值得注意,反例不需要长证明,天然适合当前模型的可靠区间。
诚实地说,这也是渐进性明显的工作:单次尝试、单一领域试点、77 条里多数尚未发表,它验证的是范式可行性,不是已经产生新数学的产量。
作者自述:每条猜想只尝试一次,多次尝试的策略没探索;bandit 式的动态分配只提了框架没实现;语料库覆盖面和各环节模型选择都会影响结果。人工复核只覆盖 77 条中的 15 条,其余 62 条的正确性只有模型裁判背书。两条具体教训:一条被 graded 为 NEW 的 Erdős 问题实际上四个月前已有人在 Erdős 问题网站上用 ChatGPT-5.2 解决,级联的搜索没找到;Lund-Saraf-Wolf 的「反例」构造本身是有限几何里的经典对象(half-tangent partition),贡献只是把它和这个猜想接上了。审稿层面,「值得发表」是模型分级,最终 77 条的命运还要看正规审稿。计费与总算力成本论文未披露,复现门槛不明。