IMO-Steps Dataset

该数据集是一个基准，包含13个IMO问题的构建块，以及20个IMO问题的完整形式化证明。主题涵盖了从整除性到有限集和函数的各种概念。所有证明步骤均使用Lean 4编写。该数据集的目的是展示当前定理证明器在解决IMO问题时的能力，并突出其优缺点。This dataset serves as a benchmark containing building blocks for 13 International Mathematical Olympiad (IMO) problems, alongside complete formalized proofs for 20 IMO problems. The covered topics span a wide range of mathematical concepts from divisibility to finite sets and functions. All proof steps are written in Lean 4. The goal of this dataset is to showcase the capabilities of contemporary theorem provers when tackling IMO problems, while also highlighting their respective strengths and limitations.

原始信息汇总

Lemmas Dataset

数据集描述

Lemmas dataset 是一个包含13个IMO问题的构建块和20个IMO问题的完整形式化证明的基准数据集。主题涵盖从可整除性到有限集合和函数的各种概念。所有证明步骤均使用Lean 4编写。

数据集构成

• 包含13个IMO问题的构建块。
• 包含20个IMO问题的完整形式化证明。
• 所有文件在Lean v4.17.0中编译无误。

证明主题

• 主题涵盖数论、代数、有限集合和函数等。

使用目的

该数据集旨在展示当前定理证明器解决IMO问题的能力，并突出它们的优点和缺点。

许可

数据集根据MIT许可证发布，欢迎通过pull requests进行贡献。

形式化的IMO问题统计

年份	问题编号	主题	是否在miniF2F中	Lean证明公开可用	证明中的Lean4代码行数
1959	P1	数论	是	是	9
1960	P2	代数	是	是	40
1962	P2	代数	是	否	60
1963	P5	代数	是	否	50
1964	P2	代数	是	是	50
1965	P2	代数	是	否	210
1968	P5	代数	是	否	30
1969	P2	代数	是	否	150
1974	P3	数论	是	否	510
1981	P6	代数	是	否	40
1982	P1	代数	是	否	75
1983	P6	代数	是	否	180
1984	P6	数论	是	否	380
1985	P6	数论	是	否	1,310
1992	P1	数论	是	否	480
1997	P5	数论	是	否	390
2007	P6	代数	是	否	570
2022	P2	代数	否	否	260
2022	P5	数论	否	否	640
2023	P4	数论	否	否	450
总计					5,884

性能指标

数据集还提供了当前最先进的LLM模型在该数据集上的性能指标。

引用

数据集、动机和附加结果可在此处找到。

版本

Lemmas Dataset明确为最新可用的Lean4版本编写，即v4.17.0。任何后续版本可能会影响发布的lemmas和某些证明可能需要未来的修订。

搜集汇总

数据集介绍

构建方式

Lemmas Dataset 是一个专门为国际数学奥林匹克（IMO）问题设计的基准数据集，其中包含了13个IMO问题的构建模块以及20个IMO问题的完整形式化证明。这些证明步骤均采用Lean 4语言编写，并且所有文件在Lean v4.17.0版本中编译无误。数据集的构建旨在展示当前定理证明器解决IMO问题的能力，并突出其优势和不足。

特点

该数据集的特点在于，它不仅提供了问题的构建模块，还提供了完整的形式化证明。这些证明覆盖了从除数到有限集合和函数的各种概念。此外，数据集遵循MIT许可，欢迎通过pull requests进行贡献。数据集中的问题按年份和主题进行了分类，便于用户查找和理解。

使用方法

使用Lemmas Dataset的方法包括：首先，用户可以从GitHub仓库克隆数据集。其次，用户需要在Lean v4.17.0环境中编译和运行这些证明文件，以验证其正确性。此外，用户可以利用数据集中的证明来评估和比较不同定理证明器的性能，例如DeepSeek Prover-v1.5-RL、Goedel-Prover等。

背景与挑战

背景概述

Lemmas Dataset是一个专注于国际数学奥林匹克（IMO）问题的基准数据集，由Roozbeh Yousefzadeh、Xuenan Cao和Azim Ospanov于2025年创建。该数据集包含13个IMO问题的构建模块以及20个IMO问题的完整形式化证明，主题涵盖从数论到有限集合和函数的多种概念。所有证明步骤均使用Lean 4语言编写，且在Lean v4.17.0版本中无编译错误。该数据集的目的是展示当前定理证明器在解决IMO问题方面的能力，并凸显其优势和不足，对相关领域产生了显著影响。

当前挑战

Lemmas Dataset在构建过程中面临的主要挑战包括：1) 形式化IMO问题的复杂性和多样性，尤其是对于难以形式化的数学概念和证明步骤；2) 在保持证明正确性的同时，提高定理证明器生成证明的效率和质量；3) 数据集的扩展和维护，随着IMO问题的不断更新，数据集需要持续更新以适应新的问题和证明技术。此外，数据集在领域问题解决方面的挑战包括：如何通过机器学习技术提高证明生成和验证的自动化水平，以及如何处理长篇证明中所需的长期规划能力。

常用场景

经典使用场景

Lemmas Dataset作为国际数学奥林匹克（IMO）问题的一个基准数据集，其经典使用场景主要在于评估和展示当前定理证明器在解决IMO问题上的能力。该数据集包含了13个IMO问题的构建块以及20个IMO问题的完整形式化证明，为研究人员提供了一种途径来测试和比较不同定理证明器在处理具有挑战性的数学问题时的性能表现。

衍生相关工作

基于Lemmas Dataset的研究已经衍生出一些相关工作，例如对最先进的语言模型在数学证明生成上的性能评估，以及探索不同证明方法和工具在解决特定类型数学问题上的有效性。这些工作不仅推动了定理证明领域的发展，也为数学和计算机科学之间的交叉研究提供了新的视角和工具。

数据集最近研究

最新研究方向

Lemmas Dataset作为一项针对国际数学奥林匹克（IMO）问题的数据集，其研究焦点集中在利用定理证明器解决数学难题的能力上。该数据集不仅包含了13个IMO问题的构建模块，还提供了20个IMO问题的完整形式化证明。研究领域涉及从数论到有限集合和函数等多个概念。近期研究利用此数据集评估了最先进的语言模型在生成数学证明方面的表现，揭示了其在处理不同难度和长度的数学证明时的优势和局限性。此数据集的发布对于推动数学定理自动证明领域的发展具有重要意义，为研究者在定理证明和数学问题解决方面的研究提供了宝贵的资源。