Search code, repositories, users, issues, pull requests...
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, and Metamath (targeting also Hol Light and Isabelle).
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.
Each problem is represented by a unique name and a file for each of the formal systems we target. Each file consists at minima in the problem statement and optionally one or more example proofs associated with it. The benchmark is divided in two splits:
Naming conventions are still a work in progress. Olympiads problems are generally named after their competition year and problem number (eg. imo-1990-p3 or aime-1983-p2). Problems coming from a particular dataset (eg the MATH dataset) are named to ease their retrieval (eg. mathd-algebra-125). Other problems are prefixed by a category hint and a unique name in the style of Metamath naming conventions (eg. induction-11div10tonmn1ton).
