问题本身即问题：迈向可扩展的数学发现

# 问题本身即是关键：迈向可扩展的数学发现  
来源：https://arxiv.org/html/2608.16977  

张盛桐¹，杰里米·阿维加德，普拉萨德·泰塔利，肖恩·韦勒克  
¹所属机构：Anysphere Co.  
²所属机构：卡内基梅隆大学  
联系邮箱：{zeyuzhen, avigad, ptetali, swelleck}@andrew.cmu.edu，[email protected]  
项目地址：https://github.com/zeyu-zheng/FAR  

###### 摘要  
人工智能系统正日益具备参与数学研究的能力。在实际研究中，前沿模型的推理能力是一种有限资源，而专家的数学评审资源则更为稀缺。因此，高效分配这些稀缺资源成为推动AI辅助数学发现高效化的关键。当前大多数AI数学工作流将人力集中在起始和结束阶段——即选择合适的研究问题，以及后续评审研究成果。这两个阶段正成为研究级数学发展的瓶颈。为此，我们提出一种新的人机发现范式。人类输入不再是预先选定的单一问题，而是专家感兴趣且具备专长的研究方向。系统随后在广泛的文献库中搜索该方向下的候选问题。受搜索引擎和推荐系统启发，我们构建了Find, Attempt, and Recommend（FAR）系统，这是一个从文献到评审的级联系统，能够自动搜索合适问题，并将人类注意力集中在通过多阶段筛选的成果上。在组合数学的试点中，该流程从5,245篇组合数学论文出发，提取出6,453个候选猜想或未解决问题，并筛选出4,717个表述清晰且仍未解决的猜想。后续的推理和自动分拣阶段产生了598个潜在解答¹，最终选定77项内容供作者团队评审。其中，我们发现了许多有趣的成果，包括针对Davies–Jenssen–Perkins–Roberts猜想、Erdős–Straus问题、Ikenmeyer–Pak–Panova猜想以及Lund–Saraf–Wolf问题的结果。这些结果证明了这种新的人机协作模式在数学发现中的有效性。  

## 1 引言  
人工智能系统在数学研究方面的贡献能力日益增强，近期在数学推理基准测试（Hendrycks等, 2021；Zheng等, 2021；Guo等, 2025；Shao等, 2025）、形式化定理证明（Trinh等, 2024；Chervonyi等, 2025；Hubert等, 2026；Ren等, 2025；Xin等, 2025；Chen等, 2025；Seed, 2026）以及特定研究级问题（OpenAI, 2026；Alon等, 2026；Tsoukalas等, 2026；Team, 2026）方面均取得了进展。  

大多数现有系统采用问题级接口：研究人员提供定理、猜想或形式化目标，系统尝试求解，最后输出结果并接受检验。这种接口虽实用，却忽略了研究中不可或缺的一环：决定哪些问题值得最初尝试。  

我们从AI辅助数学发现中的“努力分配”角度研究“选择哪些问题进行尝试”这一决策。前沿模型的推理能力和专家评审资源有限，其价值取决于哪个猜想能获得这些资源。我们不主张将推理和评审精力集中于少数预先选定的问题，而是提出一种新的工作流：专家指定研究方向，AI系统自动寻找值得投入努力的问题（图1）。  

我们构建了Find, Attempt, and Recommend（FAR）系统，一个从文献到评审的级联系统。给定一个广泛的数学主题，FAR从大型文献库中查找相关的未解决猜想，尝试证明或证伪它们，并将有希望的猜想-解答对推荐给专家评审。  

图1：从选择问题到选择方向。上部为问题级接口；下部为我们的方法。  

图3展示了FAR的详细结构。我们在组合数学领域实例化该工作流。从51,110篇数学论文出发，该流程识别出5,245篇组合数学论文，从2,742篇论文中提取出6,453个候选猜想或未解决问题，筛选后得到4,717个表述清晰且仍未解决的猜想。首次广泛的尝试运行覆盖了全部4,717个猜想。自动分拣产生了598个潜在解答，最终选择步骤选出77项供内部作者团队评审。我们手动检查了其中15项成果（基于我们自身的兴趣）。这些成果包括对Davies–Jenssen–Perkins–Roberts猜想和Lund–Saraf–Wolf猜想的反例，对Ikenmeyer–Pak–Panova关于对称群特征猜想的证明，以及对Erdős–Straus关于二项式系数整除性问题的解答。  

我们研究了在流程中分配求解尝试预算的各种策略。我们将分配建模为一个受限优化问题，并推导出最大化质量与重要性概念的策略。研究表明，与均匀基线相比，这些策略能产生更多成功的成果。此外，最优策略取决于目标：例如，若以最大化成功成果数量为目标与最大化所有成果的重要性为目标，所需策略会有所不同。  

总之，我们的贡献如下：  

- • 我们将可扩展的AI辅助数学发现表述为对一组有趣数学问题的“努力分配”问题，提出了一种能高效利用前沿模型推理与专家数学评审的人机协作范式。  
- • 受搜索引擎和推荐系统启发，我们引入了Find, Attempt, and Recommend（FAR）系统，从数学文献构建此问题池，并将模型尝试转化为可供评审的成果。  
- • 我们在组合数学试点中实例化该工作流，并分析了从文献到评审的漏斗，包括分配模型尝试的策略。  
- • 我们获得了经过作者评审的、来自组合数学文献的问题解，涵盖证明、反例以及对开放式问题的解答。相关撰文收录于附录C。  

## 2 动机与相关工作  
### 2.1 AI在数学研究中的应用  
近期AI系统在数学研究中“问题或目标已确定之后”的部分取得了快速进展。例如，FunSearch和AlphaEvolve搜索新的数学构造、程序和算法（Romera-Paredes等, 2024；Novikov等, 2025）。AlphaProof Nexus研究针对未解决研究级问题的形式化证明搜索（Tsoukalas等, 2026）。Aletheia、Rethlas、QED等近期流程探索了尝试未解决数学问题的自主或半自主工作流（Feng等, 2026；Ju等, 2026；An等, 2026；Peng等, 2026）。  

前沿模型也对单个长期研究兴趣问题做出了贡献，包括OpenAI对“单位距离问题”的证伪以及Fable辅助对“雅可比猜想”给出反例（OpenAI, 2026；Alon等, 2026；Alpöge, 2026；Bukh等, 2025）。  

相关工作中，“AI数学合作者”（Zheng等, 2026）开发了一个协作框架，其中AI代理执行并行工作流，而数学家指导研究过程。  

这些工作共同指向了陶哲轩所描述的“从证明稀缺到证明丰裕”的转变（Tao, 2026）。  

然而，数学研究很少从孤立的命题开始。在尝试解决问题之前，研究人员通常需要研究感兴趣的方向，找出其中重要的问题，并决定这些问题是否值得持续思考。这些步骤是数学工作的常规部分，但大多超出了当前AI数学系统的范围。在目前AI用于数学的研究中，模型推理前后的人类工作——问题选择与专家评审——正成为流程中的狭窄部分。  

我们的方法将AI辅助的起点移到数学研究的更早阶段。数学家不再为系统选择具体问题，而是指定一个研究方向。系统搜索可用的文献库，大规模地恢复并尝试该方向下的候选问题，返回少量成果供数学评审。这种转变类似于从执行指定任务的任务驱动代理，转向更主动的、帮助发现值得追求任务的系统。人类指定的方向约束了系统的主动性，并使搜索与数学家的兴趣及领域专业知识保持一致。数学家仍负责验证和报告任何由此产生的数学论断。  

### 2.2 构建可尝试的问题池  
研究方向本身并不能为系统提供一组可尝试的问题。诸如PutnamBench、FrontierMath和FirstProof等数学基准提供了清晰、自包含的问题池。在软件工程（LLM代理的另一个主要领域）中，GitHub提供了集中化、结构化的仓库、问题、文档和可执行软件集合，SWE-bench和ProgramBench等基准便由此构建。  

数学确实有价值合集，包括Open Problem Garden、AIM问题列表和Formal Conjectures。然而，它们的覆盖范围是选择性的，并且不是记录数学问题及其研究背景的主要基础设施。许多此类信息仍分散在文献中。一个猜想可能以编号陈述、问题、评论、未解决案例或嵌入局部符号的句子形式出现，其状态在发表后也可能发生变化。  

因此，构建一个可尝试的问题池需要从其源上下文中恢复候选陈述，并检查它们是否表述清晰且未解决。我们借鉴搜索引擎和推荐系统来组织这一过程。构建可尝试的问题池类似于候选检索，即使用不完美的信号从大型语料库中恢复陈述，并根据其来源、表述清晰度和当前状态进行过滤。  

我们还借鉴了推荐级联系统的思想，通过逐步更具选择性的阶段，将大量候选对象缩减为少量供专家关注的成果。我们的技术也与“基于文献的发现”相关，后者在已发表的知识中寻找从单篇论文中无法看到的研究机会。  

我们的目标不同于自动猜想生成——这是一项互补的工作，旨在创造新的数学猜想而非发现现有猜想。这条路线包括自动理论形成、拉马努金机器以及数据驱动的TxGraffiti系统。近期的LLM工作使用生成的猜想来扩展形式化训练数据，并将猜想生成与证明相结合，如LeanConjecturer和STP，而Moonshine则将猜想生成作为自主数学研究代理的组织目标。  

相反，我们恢复的是作者已置于文献中的未解决陈述。每个候选猜想都保留了其源论文、陈述文本、局部上下文和状态证据，以便后续的尝试和评审可以依据原始主张进行核对。状态检查后，得到的是一个由基于来源的、表述清晰且仍未解决的猜想构成的可尝试问题池P。  

### 2.3 不确定性下的努力分配  
设U为可以用自然语言表达的数学问题宇宙。人类数学研究实践可以看作在U上的大规模努力分配过程。数学家在此空间中搜寻值得探索的问题，然后尝试回答或取得进展。  

随着AI代理成为数学尝试的主要来源，分配代理算力引发了类似问题。与此同时，《莱顿宣言》强调数学家仍负责验证和报告数学论断，因此……