Formal Conjectures

Formal Conjectures是由谷歌DeepMind等机构联合创建的一个动态演进的形式化数学基准数据集，旨在为自动化推理系统提供研究级数学问题的精准评估。该数据集包含2615条使用Lean 4形式化的数学命题，其中涵盖1029个开放猜想用于零污染证明发现，以及836个已解决问题用于自动形式化验证，数据源自Erdős问题集、维基百科、学术论文及MathOverflow等多个活跃数学研究领域的权威资料库。其构建过程采用协作式开源管道，通过三级误形式化分类法确保形式化保真度，并引入了answer(sorry)机制以分离答案发现与证明验证。该数据集主要应用于人工智能驱动的数学定理自动证明与形式化验证领域，致力于解决现有基准存在的数据泄露、评估不透明及推理过程简化等核心挑战，推动研究级数学的自动化推理前沿发展。

Formal Conjectures is a dynamically evolving formal mathematical benchmark dataset jointly created by Google DeepMind and other institutions, aiming to provide accurate evaluation of research-grade mathematical problems for automated reasoning systems. This dataset contains 2615 mathematical propositions formalized using Lean 4, including 1029 open conjectures for zero-contamination proof discovery and 836 solved problems for automated formal verification. The data is sourced from authoritative repositories across active mathematical research fields such as the Erdős Problem Set, Wikipedia, academic papers, and MathOverflow. Its construction adopts a collaborative open-source pipeline, ensures formalization fidelity via a three-level misformalization taxonomy, and introduces the `answer(sorry)` mechanism to separate answer discovery from proof verification. This dataset is primarily applied in the field of AI-driven automated theorem proving and formal verification of mathematical theorems, aiming to address core challenges of existing benchmarks including data leakage, opaque evaluation, and oversimplified reasoning processes, and advance the cutting-edge of automated reasoning for research-level mathematics.

原始信息汇总

数据集概述：Formal Conjectures

地址：https://github.com/google-deepmind/formal-conjectures

1. 数据集简介

Formal Conjectures 是一个将数学中的猜想（Conjectures）用 Lean 证明助手进行形式化陈述（即只形式化陈述，不包含证明）的集合。该项目使用 mathlib 库。

2. 数据集目标

• 为自动化定理证明器和自动化形式化工具提供基准测试。
• 通过形式化过程澄清猜想的确切含义。
• 通过突出所需定义，鼓励扩展 mathlib 库。

3. 数据集特点

• 仅形式化陈述：集合中只包含形式化的猜想陈述，不包含证明。
• 形式化准确性：项目依赖人工审查贡献，并计划定期利用 AlphaProof 帮助识别潜在的形式化错误。
• 版本管理：
  • 每个月的 mathlib 标记版本，不跟踪 mathlib master。
  • 在 main 分支更新时自动添加形如 v4.{X}.{Y} 的 Git 标签。
  • 稳定基准快照使用 bench-v{N}-lean4.{X}.{Y} 格式标记，其中 v{N} 表示基准版本（添加/移除问题或修正错误时更新），lean4.{X}.{Y} 表示 Lean 4 工具链版本。标签不可变，修正错误会进入新版本 v{N+1}。

4. 目录结构

• FormalConjectures/Util：包含工具组件，如 category 属性、answer() 解释器和一些代码检查工具。
• FormalConjecturesForMathlib：包含可能适合上游到 mathlib 的代码，遵循 mathlib 的目录结构。
• 其他目录按猜想的来源类型组织。

5. 使用方式

• 这是一个 Lean 4 项目，使用 lake 管理，依赖 mathlib。
• 需要先安装 elan、lake、Lean 以及 VSCode 可选支持。
• 安装后运行： bash lake exe cache get lake build

6. 贡献方式

欢迎贡献，可以添加自己喜欢的猜想，或者通过开 issue 描述猜想。详细的贡献指南见 CONTRIBUTING.md 文件。

7. 许可协议

• 软件：Apache License 2.0
• 其他材料：Creative Commons Attribution 4.0 International License (CC-BY)
• 第三方内容：
  • 来自 Wikipedia、MathOverflow、OEIS：Creative Commons Attribution-Share-Alike License 4.0
  • 来自 bbchallenge.org：Creative Commons Attribution 4.0 International License
  • 来自 Equational Theories Project：Apache-2.0
  • 来自 arXiv：按相应论文的许可

8. 额外资源

• 文档：Formal Conjectures Documentation
• 社区交流：leanprover Zulip 上的 Formal-conjectures 频道

搜集汇总

数据集介绍

构建方式

Formal Conjectures 数据集以 Lean 4 形式语言为核心，系统性地从活跃数学研究领域中遴选问题来源，包括 Erdős 问题集、Wikipedia 猜想、Green 未解问题、学术论文及 arXiv 预印本等，覆盖数论、组合学、量子理论、代数几何等十余个 AMS 学科分类。研究者通过人工与 AI 辅助的双重形式化管线，将非正式的数学陈述编译为带有 @[category] 和 @[subject] 标签的 Lean 定理，其中开放猜想以 sorry 占位符标记，已解决问题则附有正式证明或外部证明链接。为保证形式化的准确性，项目引入三级误形式化分类体系（翻译、欠规范、源错误），并借助社区代码审查、测试引理套件及自动定理证明器的周期性运行对陈述进行迭代审计与修正，最终形成一个动态增长、持续演进的正式数学问题仓库。

特点

该数据集的核心特点在于其零污染评估环境与前沿性：包含 1029 个开放研究猜想，这些陈述在发布时尚无任何形式的已知证明，从而彻底消除数据泄露与记忆化风险，为衡量自动化推理系统的真实数学发现能力提供纯净实验场。同时，836 个已解决问题构成证明自动形式化的特有挑战，要求模型将非正式论证转化为可通过 Lean 4 内核验证的严格证据链。数据集采用版本化快照机制（如 FC100OpenSet1）与分型评价体系，支持计算预算与模型架构的灵敏度分析。此外，其 answer(sorry) 机制可分离答案发现与证明验证，而 @[formal_proof] 属性则解耦问题陈述与解决方案，保持仓库轻量化的同时链接外部验证源，充分体现了对数学精确性与实用性的双重追求。

使用方法

使用者可按两大任务路径利用该数据集：首要任务为开放猜想的新证明发现，研究者需以 Lean 4 证明项替换定理中的 sorry 占位符，并由内核自动验证正确性，这一过程完全杜绝人工评估的主观性与模糊性；次要任务为已解决问题的证明自动形式化，模型需将非正式数学论证转化为合法的 Lean 代码。为促进标准化与可复现评估，数据集提供 FC100SolvedSet1 与 FC100OpenSet1 两个冻结子集，分别对应 100 个已解决与 100 个开放问题，且通过版本标签（如 bench-v1-lean4.27.0）确保跨时间的可比性。此外，仓库作为统一 API 运行，研究人员可将新形式化的猜想提交至中心枢纽，同时供多方自动求解系统并发尝试，从而加速数学发现的协作生态构建。

背景与挑战

背景概述

随着自动推理系统与大型语言模型在形式化数学领域取得显著进展，现有测评基准面临数据泄露、评价集非公开、成功标准过于简化以及饱和化等多重困境。为应对这些挑战，Google DeepMind 与伦敦帝国理工学院等机构的研究人员于2025年提出了 Formal Conjectures 基准数据集，专注于研究级别的数学问题。该数据集收集了2615条形式化于 Lean 4 的数学命题，涵盖1029个开放猜想与836个已解问题，旨在为零污染的真实数学推理能力评估提供坚实基础。其核心贡献在于开创性地结合了开放猜想证明发现与证明自动形式化两个目标，并引入持续演进的构建方式与标准化评价框架，已实际推动多项数学新发现，对衡量与推动AI在形式数学领域的前沿能力具有重要影响力。

当前挑战

Formal Conjectures 所面对的核心领域挑战在于：如何避免已有基准常见的数据泄露和饱和问题，确保测评信号能真实反映系统的原创推理能力而非记忆。围绕开放猜想的零污染评价虽能解决此点，但同时也引入了严峻的构建挑战：精确形式化研究级数学命题极为困难，常出现翻译、语义或隐含约定层面的误形式化，需采用多层级的审查与自动验证机制加以纠正。此外，基准依赖 Lean 4 内核验证证明，虽提供了客观严明的成功标准，但内核潜在的底层缺陷或非预期公理为评价的终极严谨性留下了理论风险。构建过程中，需持续平衡社区贡献、自动定理证明器的审计反馈与版本演化间的协调，以确保基准动态更新与可重复比较之间的稳健性。

常用场景

经典使用场景

在自动推理与形式化数学的交汇领域，Formal Conjectures数据集被广泛用作评估人工智能系统在探索未解决问题时展现真实推理能力的零污染基准。其经典使用场景聚焦于两大核心任务：其一为开放猜想的全新证明发现，要求模型从零开始构造出经Lean 4内核验证的形式化证明，从而检验其处理前沿数学难题的原创性推理水平；其二为已知定理的证明自动形式化，考验模型将非形式化的数学论证精准翻译为可检验的代码的能力。通过将1029个尚未解决的开放猜想与836个已解决的数学命题整合于统一框架，该数据集为形式化定理证明的进步提供了兼具挑战性与可攀登性的测试平台。

实际应用

在实际应用中，Formal Conjectures数据集已展现出超越单纯评估的实用价值。它为数学家与人工智能系统搭建了高效协作的桥梁：研究者或自动化求解器可通过统一API直接获取并尝试解决形式化的数学猜想，而系统产生的证明或反例又反过来作为验证机制，帮助发现并修正形式化过程中的潜在错误，形成迭代优化的良性循环。例如，该基准已被用于验证亚里士多德（Aristotle）及DeepMind探索智能体等前沿系统在真实数学问题上的表现，多个开放猜想在此过程中获得了实质性进展甚至被解决。这种动态互动不仅加速了数学发现的进程，还促使模糊的非形式化问题得到澄清与精炼。

衍生相关工作

自Formal Conjectures发布以来，它已催生出一系列后续研究工作。在证明发现方面，研究者借助该基准中的形式化语句成功求解了多个开放问题，如Erdős第124号问题，这些成果被整理为独立论文发表。在评估框架层面，该数据集启发了多个子集标准（如FC100OpenSet1与FC100SolvedSet1）的建立，为不同系统间的可重复比较提供了稳定参照。此外，为支撑该基准中的复杂形式化需求，社区构建了FormalConjecturesForMathlib目录，其中包含众多补充定义与辅助引理，这些成果正持续向上游的Mathlib库贡献，从而推动了整个形式化数学基础设施的扩展与完善。