MathOlympiadBench

This repository contains the MathOlympiadBench dataset, which is introduced in the paper [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://huggingface.co/papers/2508.03613).

**Project Page:** https://blog.goedel-prover.com
**Code Repository:** https://github.com/Goedel-LM/Goedel-Prover-V2

MathOlympiadBench (**Math Olympiad**) comprises human-verified formalizations of Olympiad-level mathematical competition problems, sourced from [Compfiles](https://dwrensha.github.io/compfiles/imo.html) and [IMOSLLean4 repository](https://github.com/mortarsanjaya/IMOSLLean4). MathOlympiadBench contains 360 problems, including 158 IMO problems from 1959 to 2024, 131 IMO shortlist problems covering 2006 to 2023, 68 national mathematical Olympiad problems, and 3 additional mathematical puzzles.

MathOlympiadBench is human-processed to eliminate several issues presented in the source problems: 1. incomplete problem statements, 2. distribution across multiple files, 3. multiple theorems per problem, and 4. incompatibility with the commonly used Mathlib. The verification process ensures that each problem contains exactly one formal theorem with its corresponding informal statement, and confirms that all formal statements can pass the compilation with the *sorry* tactic.

We compared the IMO problems shared between MathOlympiadBench and MiniF2F, and identified at least 3 cases in MiniF2F exhibiting issues such as: 1. the formal statement to be proved is strictly weaker than the informal statement, and 2. the formal statement does not match the informal statement. Notably, similar issues are not observed for these problems in MathOlympiadBench.

### Sample Usage

You can download the dataset using Git LFS:

```bash
git lfs install
git clone https://huggingface.co/datasets/Goedel-LM/MathOlympiadBench
```

本仓库收录了数学奥林匹克基准数据集（MathOlympiadBench），该数据集在论文《Goedel-Prover-V2：借助脚手架数据合成与自我校正实现形式化定理证明的规模扩展》（https://huggingface.co/papers/2508.03613）中被提出。

**项目主页**：https://blog.goedel-prover.com
**代码仓库**：https://github.com/Goedel-LM/Goedel-Prover-V2

数学奥林匹克基准数据集（MathOlympiadBench，对应英文标注Math Olympiad）收录了经人工核验的奥林匹克级数学竞赛问题的形式化表述，数据源自Compfiles（https://dwrensha.github.io/compfiles/imo.html）与IMOSLLean4仓库（https://github.com/mortarsanjaya/IMOSLLean4）。该数据集共包含360道问题，其中包括1959年至2024年间的158道国际数学奥林匹克（International Mathematical Olympiad, IMO）真题、2006年至2023年间的131道国际数学奥林匹克备选题、68道国家级数学奥林匹克竞赛试题，以及3道额外的数学谜题。

本数据集经过人工处理，以修复源问题存在的四类典型问题：1. 问题描述不完整；2. 内容分散存储于多个文件中；3. 单道问题对应多条定理；4. 与当前广泛使用的Mathlib不兼容。核验流程确保每道问题仅包含一条形式化定理及其对应的非形式化表述，并确认所有形式化表述均可通过带有*sorry*策略的编译校验。

我们对比了MathOlympiadBench与MiniF2F中重合的国际数学奥林匹克真题，发现MiniF2F中至少存在3道问题存在如下问题：1. 待证明的形式化表述严格弱于非形式化表述；2. 形式化表述与非形式化表述不匹配。值得注意的是，MathOlympiadBench中的同类问题未出现上述类似问题。

### 示例用法
你可通过Git大文件存储（Git LFS）下载本数据集：
bash
git lfs install
git clone https://huggingface.co/datasets/Goedel-LM/MathOlympiadBench