问题即问题：迈向可扩展的数学发现 **摘要** 对自动定理证明和人工智能驱动数学研究的追求，很大程度上聚焦于求解已知问题。然而，让数学人工智能系统既高度精炼又能够自我改进的最快途径，或许不在于求解（即证明），而在于这一行为本身——提出新的数学问题。我们提出如下论定：推进数学发现（从已知问题中衍生出有价值的新问题）的能力，应当成为构建自动定理证明器以验证那些新生成问题的一个优先驱动因素，从而形成一个自我改进的循环。这种方法的显著优势在于，用以驱动这一循环的训练数据可以从头开始生成，而无需依赖外部数据源。在本文中，我们论证，数学发现——即在新近生成的结构领域内提出可证明的猜想，而非仅在这些结构表面进行操作——正是这一自我改进循环的核心环节。我们仅使用一个命题逻辑求解器作为其自身的验证器，无需任何事先训练的数学知识，即可在此框架下训练语言模型，使其生成的猜想在不可满足的布尔公式的受限世界中得到验证。在所研究的世界中，我们验证了生成的猜想与真值表完备集（称为“结构”）相吻合，并证明了一个关键结果：即此类生成-验证循环可以产生任意精炼的验证器，且所生成的、已验证的猜想随世界规模的增大而增多。这一成果为一条通往“无数据”数学发现的可扩展路径铺平了道路，在该路径中，人工智能与形式验证器共同协作以拓展数学知识，而无需预先存在的数据集。我们引入的框架（我们称之为问题生成器）借鉴了生成对抗网络、基于模型的强化学习与数据同化方法，为在一个可扩展且自洽的环境中实现机器驱动发现提供了蓝图。

摘要

人工智能系统正日益有能力为数学研究作出贡献。在研究实践中，前沿模型的推理能力是一种有限资源，而专家数学审阅更是极为稀缺。因此，如何合理分配这些稀缺资源，是提升人工智能辅助数学发现效率的核心问题。在目前大多数人工智能数学工作流中，人力投入集中于起始和收尾两个阶段，即选题阶段与对最终产出成果的审阅阶段。这两个环节正成为研究级数学的瓶颈。我们针对这一问题提出了一种新的人机协同发现范式。人类输入不再是一个预先选定的单一问题，而是一个专家具备研究兴趣和专业知识的科研方向。系统随后在该方向上对广泛的文献语料库进行搜索，以发现候选问题。受搜索与推荐系统的启发，我们构建了“发现—尝试—推荐”（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等人猜想与问题的研究成果。这些结果表明，这种人机协作新模式对于数学发现是有效的。

English

AI systems are increasingly capable of contributing to mathematical research. In research practice, frontier-model reasoning is a limited resource, and expert mathematical review is even more sharply constrained. Allocating these scarce resources well is therefore central to making AI-assisted mathematical discovery efficient. In most current AI-for-math workflows, human effort is concentrated at the beginning and end, in selecting suitable research problems and later reviewing the resulting artifacts. These two stages are becoming bottlenecks for research-level mathematics. We address them by proposing a new human-AI discovery paradigm. The human input is no longer a single problem selected in advance, but a research direction in which the experts have interest and expertise. The system then searches a broad literature corpus for candidate problems in that direction. Inspired by search and recommender systems, we build Find, Attempt, and Recommend (FAR), a literature-to-review cascade that automates the search for suitable problems and focuses human attention on artifacts that have passed several stages of filtering. In a combinatorics pilot, the pipeline starts from 5,245 combinatorics papers, recovers 6,453 candidate conjectures or open problems, and filters them to 4,717 apparently well-posed and still-open conjectures. Subsequent reasoning and automated triage stages surface 598 potential resolutions and select 77 items for author-team review. Among them, we identify many interesting discoveries, including results on conjectures and questions of Davies--Jenssen--Perkins--Roberts, Erdős--Straus, Ikenmeyer--Pak--Panova, and Lund--Saraf--Wolf. These results demonstrate the effectiveness of this new mode of human-AI collaboration for mathematical discovery.