license:mit math theorem-proving arxiv:2109.00110 region:us
MiniF2F is a formal mathematics benchmark (translated across multiple formal systems) consisting of exercise statements from olympiads (AMC, AIME, IMO) as well as high-school and undergraduate maths classes.

This dataset contains formal statements in Isabelle. Each statement is paired with an informal statement and 
an informal proof, as described in Draft, Sketch, Prove [Jiang et al 2023].

The problems in this dataset use the most recent facebookresearch/miniF2F commit on July 3, 2023.
@inproceedings{jiang2023draft,
    title={Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs},
    author={Albert Qiaochu Jiang and Sean Welleck and Jin Peng Zhou and Timothee Lacroix and Jiacheng Liu and Wenda Li and Mateja Jamnik and Guillaume Lample and Yuhuai Wu},
    booktitle={The Eleventh International Conference on Learning Representations },
    year={2023},
    url={https://openreview.net/forum?id=SMa9EAovKMC}
}

@inproceedings{zheng2022miniff,
    title={miniF2F: a cross-system benchmark for formal Olympiad-level mathematics},
    author={Kunhao Zheng and Jesse Michael Han and Stanislas Polu},
    booktitle={International Conference on Learning Representations},
    year={2022},
    url={https://openreview.net/forum?id=9ZPegFuFTFv}
}
---
license: mit
tags:
- math
- theorem-proving
---

## Dataset Description

- **Point of Contact:** [Sean Welleck](https://wellecks.com/)

# miniF2F+informal in Isabelle
[MiniF2F](https://arxiv.org/abs/2109.00110) is a formal mathematics benchmark (translated across multiple formal systems) consisting of
exercise statements from olympiads (AMC, AIME, IMO) as well as high-school and undergraduate maths
classes.

This dataset contains formal statements in Isabelle, each paired with an informal statement and 
an informal proof as described in [Draft, Sketch, Prove [Jiang et al 2023]](https://openreview.net/forum?id=SMa9EAovKMC).

This dataset is derived from the latest [facebookresearch/miniF2F commit](https://github.com/facebookresearch/miniF2F/tree/5271ddec788677c815cf818a06f368ef6498a106) as of July 3, 2023.
Please see the repository for additional information.

### Licensing Information

MIT

### Citation Information

This dataset contains Isabelle problem statements from the miniF2F benchmark along with informal statements and proofs.

The initial version of miniF2F is described in [Zheng et al ICLR 2022](https://arxiv.org/abs/2109.00110):
```
@inproceedings{zheng2022miniff,
    title={miniF2F: a cross-system benchmark for formal Olympiad-level mathematics},
    author={Kunhao Zheng and Jesse Michael Han and Stanislas Polu},
    booktitle={International Conference on Learning Representations},
    year={2022},
    url={https://openreview.net/forum?id=9ZPegFuFTFv}
}
```

The informal statements and proofs were curated and described in [Draft, Sketch, and Prove; Jiang et al ICLR 2023](https://openreview.net/forum?id=SMa9EAovKMC), along with significant fixes and improvements to the initial version of miniF2F:
```
@inproceedings{jiang2023draft,
    title={Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs},
    author={Albert Qiaochu Jiang and Sean Welleck and Jin Peng Zhou and Timothee Lacroix and Jiacheng Liu and Wenda Li and Mateja Jamnik and Guillaume Lample and Yuhuai Wu},
    booktitle={The Eleventh International Conference on Learning Representations },
    year={2023},
    url={https://openreview.net/forum?id=SMa9EAovKMC}
}
```


