Bug reports and update policy for facebookresearch/miniF2F

Note: This repository is a fork of the original OpenAI miniF2F repository https://github.com/openai/miniF2F, with additional data and many formal statement fixes.

If you find errors in the statement formalizations, please submit a pull request. We will continue updating the dataset. Please cite the version you used by commit or date for reproducible evaluations.

We will not accept pull requests with additional proofs to reduce test set contamination.

Overview

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.

The goal of the project is to provide a shared benchmark to evaluate and directly compare automated theorem proving systems based on the formal systems targeted, initially Lean, Isabelle, and Metamath (targeting also Hol Light).

The benchmark (released under permissive licenses (MIT for Metamath, Apache for Lean)) is a work in progress and contributions are welcome and encouraged through pull requests.

Citation

The initial version of the benchmark is described in detail in the following pre-print:

@article{zheng2021minif2f,
  title={MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics},
  author={Zheng, Kunhao and Han, Jesse Michael and Polu, Stanislas},
  journal={arXiv preprint arXiv:2109.00110},
  year={2021}
}

The original repo is miniF2F. It has then seen significant fixes and improvements, notably the addition of an informal statement and an informal proof for each problem. The curation of the informal component is described in the following paper. To cite it:

@inproceedings{
  2210.12283,
  title={Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs},
  author={Albert Q. Jiang and Sean Welleck and Jin Peng Zhou and Wenda Li and Jiacheng Liu and Mateja Jamnik and Timothée Lacroix and Yuhuai Wu and Guillaume Lample},
  booktitle={Submitted to The Eleventh International Conference on Learning Representations},
  year={2022},
  url={https://arxiv.org/abs/2210.12283}
}

We decided to start a separate repository, instead of submitting PRs, for better maintainence of the dataset.

Statistics

Example problem statement (mathd_algebra_17)

Informal

Solve for