This repository is a fork of openai/miniF2F, which is described in MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics.
It contains Lean 4 translations of the Lean 3 problems in the original, translated using mathport.
Compared to the original, this:
-
contains natural language docstrings taken from (best estimates of) the source of the original problems, to make identification of misformalizations easier.
These descriptions originate from some combination of:
- The contest collection question archive on the AoPS forums
- The MATH dataset
-
has many fewer misformalizations, with all known false statements removed, and many statements strengthened to match the strength of the english statement.
-
simplifies the
Minif2fImportstrategy, instead importing all of mathlib.
This is the version of the benchmark on which AlphaProof is evaluated.
This is not an official Google product.