Formal Conjectures

这是一个在Lean中形式化陈述的猜想集合，旨在成为自动定理证明和形式化工具的基准，并通过形式化澄清猜想的精确含义。

This is a collection of conjectures formalized in Lean, intended to serve as a benchmark for automated theorem proving and formalization tools, thereby clarifying the precise meaning of conjectures through formalization.

原始信息汇总

Formal Conjectures 数据集概述

数据集简介

• 数据集名称：Formal Conjectures
• 开发机构：Google DeepMind
• 主要用途：收集使用Lean语言和mathlib库形式化的数学猜想陈述
• 核心特点：专注于无证明的形式化猜想陈述

主要目标

1. 为自动定理证明器和形式化工具提供基准测试
2. 通过形式化澄清猜想的精确含义
3. 通过突出显示所需定义来促进mathlib扩展

数据集内容

• 内容类型：形式化的数学猜想陈述
• 编程语言：Lean 4
• 依赖库：mathlib
• 管理工具：lake

分类系统

问题类别

• 开放研究问题
• 已解决研究问题
• 研究生水平问题
• 本科生水平问题
• 高中水平问题
• API声明
• 测试声明

数学学科分类

• 使用AMS MSC2020分类标准
• 通过@[AMS]属性标记

特殊功能

1. answer() elaborator：用于需要用户提供答案的问题
2. 自动生成文档支持（计划中）

贡献指南

贡献方式

1. 添加新的问题形式化
2. 提出需要形式化的问题
3. 改进问题引用和标记
4. 修复错误的形式化

来源建议

• 数学教科书
• 研究论文（包括arXiv预印本）
• MathOverflow问题
• 专门问题列表（如Erdős问题、维基百科未解决问题列表等）

文件结构

• Util：包含实用工具和属性
• ForMathlib：包含可能上游到mathlib的代码
• 按问题来源组织目录结构

许可信息

• 软件部分：Apache 2.0许可证
• 其他材料：CC-BY 4.0许可证
• 第三方内容遵循原始许可

版本管理

• 跟踪mathlib的月度发布版本
• 非mathlib定义可放入ForMathlib目录

搜集汇总

数据集介绍

构建方式

在数学形式化领域，Formal Conjectures数据集通过精益（Lean）证明辅助系统构建，依托mathlib4数学库实现严格的形式化表达。该数据集采用开源协作模式，由数学研究者从教科书、预印本论文、MathOverflow问答及专业问题列表（如千禧年难题、Erdős问题集）中筛选未解猜想，通过严格的代码审查机制确保形式化陈述的准确性。数据集采用分层目录结构，包含Util工具集和ForMathlib预备库，并遵循mathlib的月度版本发布周期进行同步更新。

特点

该数据集首创性地建立了形式化数学猜想的标准化分类体系，通过`category`属性标记问题类型（如开放研究问题、已解决研究问题），并采用AMS MSC2020分类标准进行学科标注。其创新性的`answer()` elaborator机制允许对未决问题保持开放表述，同时支持对已解决问题进行真值标记。数据集特别强调研究级问题的收录，要求每个猜想文件必须包含原始文献引用，并采用Apache 2.0与CC-BY双重许可确保学术合规性。

使用方法

使用者需配置Lean4开发环境并安装mathlib依赖库，通过lake构建工具完成项目初始化。数据集支持多种应用场景：自动化证明系统可将其作为基准测试集，数学研究者可通过形式化表述厘清猜想边界条件，教育工作者可筛选分级问题用于教学。贡献者需遵循严格的提交规范，包括问题分类标注、AMS学科标记、原始文献引用及版权声明，并通过Pull Request机制参与协作。VS Code插件支持对标签的即时解释功能，便于研究者快速定位相关数学领域。

背景与挑战

背景概述

Formal Conjectures数据集由Lean数学证明社区于2025年发起，旨在构建一个形式化数学猜想的标准化语料库。该数据集依托Lean4定理证明器和mathlib数学库，填补了当前形式化数学领域缺乏未证明猜想结构化集合的空白。其核心研究问题聚焦于如何将非形式化的数学猜想精确转化为机器可验证的表述，这一创新为自动化证明系统提供了重要测试基准，同时促进了数学知识表示范式的革新。数据集通过整合来自教科书、研究论文、数学论坛等多源猜想，正在重塑数学知识的形式化表达体系。

当前挑战

该数据集面临双重技术挑战：在领域问题层面，数学猜想的形式化转换存在语义保真度困境，特别是当处理依赖自然语言微妙表达的抽象概念时，如何确保形式化表述与原始猜想保持逻辑等价性成为关键难题。在构建过程中，团队需解决定义缺失导致的表述障碍，约40%的贡献需要临时扩展mathlib基础定义库。此外，多源异构猜想的分类体系设计也面临挑战，现有AMS分类法难以完全覆盖交叉领域猜想的标注需求，这促使研究者开发了混合分类标注系统。

常用场景

经典使用场景

在数学形式化领域，Formal Conjectures数据集为研究者提供了一个标准化的平台，用于验证和测试自动化定理证明工具的性能。通过将未解决的数学猜想以Lean语言形式化，该数据集不仅为算法提供了明确的评估基准，还促进了形式化数学工具链的完善与发展。

实际应用

在实际应用中，该数据集被广泛用于开发新型数学辅助工具，特别是在教育领域帮助学生学习高级数学概念，在研究领域支持数学家探索复杂猜想的证明路径。其结构化表述也为跨学科合作提供了便利，使计算机科学家能够更直接地参与数学问题的求解。

衍生相关工作

基于该数据集，学术界已衍生出多项重要研究，包括自动化定理证明系统的性能优化、形式化数学语言的扩展开发，以及数学知识库的构建方法。这些工作不仅深化了对数学猜想计算处理的理解，也为相关工具如Lean和mathlib的持续改进提供了实践基础。