形式化猜想：数学中可验证发现的开放且持续演进的基准

# 形式化猜想：一个开放且不断演进的数学验证发现基准  
来源：https://arxiv.org/html/2605.13171  

[e省略lean4设置]  

Moritz Firsching¹, Paul Lezeau¹², Salvatore Mercuri¹², Miklós Z. Horváth¹, Yaël Dillies³, Calle Sönne¹, Eric Wieser¹, Fred Zhang¹, Thomas Hubert¹, Blaise Agüera y Arcas⁴, Pushmeet Kohli¹  

¹Google DeepMind, ²帝国理工学院, ³斯德哥尔摩大学, ⁴Google  

###### 摘要  

随着自动推理系统的快速进步，衡量其能力需要研究级别的形式化数学问题。为此，我们提出了**形式化猜想（Formal Conjectures）**¹¹¹https://github.com/google-deepmind/formal-conjectures，这是一个不断演进的基准，目前包含 2615 个用 Lean 4 形式化的数学问题陈述。这些数据来源于活跃的数学研究领域，包括 1029 个开放研究猜想（提供零污染的数学证明发现基准）和 836 个已解决问题（用于证明的自动形式化）。值得注意的是，该仓库提供了一个结构化接口，将进行问题形式化和澄清的数学家与试图解决问题的AI系统及人类连接起来。该基准已展现出直接效用，被用于取得新的数学发现，包括解决开放研究猜想。我们描述了一个协作式开源项目中确保这些形式化正确性的方法，该项目受益于活跃社区的贡献。在此框架下，AI生成的证明和反证作为有价值的审计机制，用于迭代提升基准的保真度。最后，我们提供标准化的评估设置，并在冻结的评估子集上报告基线结果，展示了一个可攀登的信号，用于衡量当前自动推理在研究级数学上的前沿水平。  

## 1 引言  

随着自动推理系统（包括大型语言模型）能力的不断提升，用于衡量其进步的基准面临重大挑战。在（形式化）数学领域，许多现有评估框架存在以下问题：（i）**数据泄露**：基准问题的解出现在网络上，使得难以区分真正的推理与记忆。这对诸如 Zheng 等人 (2021)、Tsoukalas 等人 (2024)、Jiang 等人 (2025)、Yu 等人 (2025) 的基准构成挑战。（ii）**秘密评估**：为防止泄露，一些基准要求评估集保持私有，这阻碍了开放可重复的研究（Chollet 等人，2025；Glazer 等人，2024；Center for AI Safety 等人，2026）。（iii）**过于简化的成功标准**：许多基准依赖验证一个简单的、机器可检查的最终答案（如一个数字），这无法捕捉完整数学证明中固有的复杂多步推理（Hendrycks 等人，2021；Glazer 等人，2024）。（iv）**饱和**：随着模型改进，一些基准变得饱和。例如，MiniF2F (Zheng 等人，2021) 现在常规解决率超过 99%；参见 Hubert 等人 (2025)、Chen 等人 (2025b)、Lin 等人 (2025)。为应对这些局限，我们引入 **形式化猜想**，一个开源且不断增长的数学问题集合，使用 Lean 4 (Moura 和 Ullrich，2021) 及 Mathlib (The mathlib Community，2020) 进行形式化。该基准主要挑战是**开放猜想**，提供一个零污染测试平台，其解无法在现有训练数据中找到。次要挑战包括（非形式化）已解决问题，用于自动形式化，这些不具备相同的零污染保证。我们使用形式语言形式化所有问题，以实现客观、严格和自动化评估：一个提议的解被内核接受且不依赖禁止公理（如 `sorry`）时，即被确认为正确。我们选择 Lean 4 是出于实用考虑：Mathlib 作为最大的可用形式化数学库，对于陈述各种高级猜想至关重要。虽然我们专注于 Lean 4，但基准的核心原则与语言无关，可扩展到其他形式化系统。本文详细介绍了**形式化猜想**基准的构建和方法论。该基准以 Apache 2.0 许可证公开，并已被用于现实世界的数学发现 (Alexeev 和 Mixon，2025；DeepMind，2026)。总结我们的主要贡献如下：  

- **• 形式化猜想基准**：一个大规模、不断演进的数据集，包含 2615 个 Lean 4 数学陈述，包括 1029 个开放猜想（用于零污染证明发现）和 836 个已解决问题（用于自动形式化）。  
- **• 统一的数学推理 API**：一个仓库接口，连接数学家与自动求解器生态系统，以促进同时进行的陈述审计和问题快速分发给AI系统。  
- **• 陈述形式化方法论**：我们引入一个协作流水线和三级误形式化分类法（翻译、欠指定、来源），以确保形式化保真度。这包括 `answer`（`sorry`）机制，将数学价值发现与证明验证解耦。我们提供了 291 个研究级形式化修正案例的见解。  
- **• 标准化评估框架**：我们提供了一个使用 Lean 4 内核的严格评估设置，以验证多步推理，而不依赖过于简化的数值答案。我们建立了冻结子集 `FC100SolvedSet1` 和 `FC100OpenSet1`，以实现稳定、可复现的模型比较。  

## 2 相关工作  

我们的工作涉及数学推理基准和形式化定理证明的交集。  

##### 通用数学推理基准。  

多个基准在不要求形式化证明的情况下评估AI系统的高级问题求解能力。FrontierMath (Glazer 等人，2024) 使用专家制作的问题，通过数值答案验证，虽然机器可检查，但未完全捕捉多步推理过程。2026年1月，Epoch AI 推出了 *FrontierMath: Open Problems*，这是一个仅限网站的小型试点，包含一些未解决的研究级非形式化问题，并提供评估服务。人类最后一次考试 (Center for AI Safety 等人，2026) 众包专家问题，但依赖答案检查而非证明验证。MathArena (Balunović 等人，2025) 在新竞赛问题上评估LLM以减少污染风险，并评估非形式化证明写作。ARC Prize (Chollet 等人，2025, 2026) 针对抽象推理，与我们关注测量超越模式匹配的真实推理一致。相比之下，形式化基准允许自动验证完整推理或证明。  

##### 形式化数学基准与自动定理证明。  

对自动定理证明的兴趣加速了AI推理的发展，导致现有形式化基准的迅速饱和。MiniF2F (Zheng 等人，2021) 开创了高中水平评估，但随着模型改进变得饱和。这一转变由 AlphaProof (Hubert 等人，2025) 和 AlphaGeometry 2 (Chervonyi 等人，2025) 在2024年IMO中获得银牌表现定义，其中 AlphaProof 解决了 Lean 问题并引入了 Formal-IMO (Hubert 等人，2025) 数据集。像 Aristotle (Achim 等人，2025) 和 Seed-Prover (Chen 等人，2025b) 的系统在2025年IMO中达到金牌等效。这种能力飞跃级联到本科生数学，像 PutnamBench (Tsoukalas 等人，2024) 和 Putnam 2025 等基准正被 Seed-Prover 1.5 (Chen 等人，2025a)、Numina (Liu 等人，2026) 及其他工业系统饱和。虽然 SorryDB (Letson 等人，2026) 评估AI在实用定理补全上的表现，FATE (Jiang 等人，2025) 针对前沿代数的不同难度，但早期基准的饱和凸显了对研究级评估的迫切需求：在未解决的研究级数学上对推理进行基准测试。  

##### 形式化猜想的采用。  

自2025年5月开源发布以来，该仓库已被数学家和工具开发者所采用。Boris Alexeev 使用仓库的形式化，通过 Aristotle (Achim 等人，2025) 证明了 Erdős 问题 124 (Bloom，2025)。尽管该陈述最初被误形式化并包含一个意外的额外假设，但 Aristotle 的证明在没有依赖该假设的情况下成功。后续许多成功案例，如 (Alexeev 和 Mixon，2025)，突出了仓库对于发现的价值，并展示了AI生成的证明如何作为关键的审计机制来提升形式化保真度。一个 DeepMind 证明智能体 (DeepMind，2026) 对整个仓库进行了系统评估，解决了一些开放问题。为了促进标准化、可复现的评估，本文引入了命名、版本化的快照（第4.1节），将评估从单个测试推进到跨多种方法的系统基准测试。  

## 3 形式化猜想  

### 3.1 问题选择与组成  

**非形式化来源问题分布：** Erdős 问题 1318、Wikipedia 476、Green 的开放问题 175、论文 131、开放量子问题 125、Wall II 110、OEIS 105、arXiv 56、MathOverflow 53、其他来源 66。混合了现有档案、研究收藏和开放问题列表。  

**形式化猜想基准：**  
- 研究开放 (1029) → 主要目标：新证明发现（零污染的真实推理测试平台）  
- 研究已解决 (836) → 次要目标：自动形式化  
- 所有其他陈述 (750)  
  - 测试 (467)  
  - API (155)  
  - 教科书 (128) → 目的：完整性检查与定义测试  

**形式化流水线**  

图1：左：非形式化来源分布。右：形式化类别分布，包括开放 (1029) 和已解决 (836) 问题。  

图2：仓库随时间增长。  

该基准的问题来源于多样的数学文献以获得广泛覆盖。主要来源包括 Paul Erdős 提出的问题集合（按 *erdosproblems.com* 编录，Bloom，2023）；Kourovka 笔记本中的群论未解决问题 (Khukhro 和 Mazurov，2026)；IQOQI Vienna 的开放量子问题列表 (IQOQI Vienna 和 Werner，2017)；著名的 Wikipedia 猜想；近期学术期刊和 arXiv 论文中的猜想；以及 MathOverflow 上的提问。每个非形式化来源的问题数量见图1。此外，自最初开源发布以来，仓库持续增长，如图2所示。该集合分为两个主要类别：**未解决猜想**，即开放研究问题，其形式化或非形式化证明将代表新的数学发现；**已解决问题**，即具有已知*非形式化*证明的已建立定理，用于基准测试AI形式化现有论证的能力，尽管目前只有一小部分有*形式化*证明可用。我们包含这两类不仅因为它们各自作为不同任务（证明生成和自动形式化）的基准，还因为它们常常相互交织。在形式化一个开放猜想时，自然也会陈述并证明更简单的、已解决的变体。例如，关于所有有效 \(k \in \mathbb{N}\) 存在大小为 \(4k\) 的 Hadamard 矩阵的通用猜想，可以与已解决的情况（例如所有 \(k \leq 166\)）和第一个开放情况（\(k=167\)）一起呈现。*已解决*问题的其他来源包括同时包含开放和已解决问题的猜想集合。在这些情况下，我们也会形式化已解决案例的陈述。它们通常与开放猜想在主题上相关，因此其陈述的形式化和证明的自动形式化支持了开放猜想。已解决问题集合也包括更简单的陈述，从琐碎到教科书水平，有助于验证底层形式化的正确性。包含此类简单问题有助于检测开放猜想的不正确形式化：对一个简单特例或已知变体的反证可能表明所用某些定义被错误陈述。下面的例子展示了这些初始误形式化如何改进形式化和非形式化问题陈述。我们力求始终陈述一个猜想的最简单开放变体，以及更一般的猜想。  

##### @[category] 属性  

为了便于导航，每个陈述被标记为以下类别标签之一：`researchopen`（开放研究级问题）、`researchsolved`（已解决研究级问题）、`textbook`（教科书级数学问题，范围从高中到研究生水平）、`API`（为通用重用而开发新定义的基础理论陈述）、`test`（作为完整性检查的陈述）。所有类别的分布见图1右侧。  

##### @[subject] 属性  

陈述也按照 AMS 数学学科分类 (Editors of Mathematical Reviews and zbMATH，2020) 标记主题标签。按来源集合和 AMS 学科分类的分布见表3和表4（附录A.1）。