Primary evidence
- MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicsS1 · Primary research · Paper · 2021-08-31
- OpenAI miniF2F repositoryS1 · Primary research · Benchmark
miniF2F establishes a cross-system benchmark for formal Olympiad mathematics
The benchmark translated problems from AIME, AMC, IMO and educational sources into formal languages. Its goal was not a new mathematical theorem but a reproducible common target on which learned theorem provers could be trained and compared.
What happened?
miniF2F introduced 488 formal Olympiad-level problem statements spanning Metamath, Lean and additional proof assistants, with held-out splits intended for cross-system theorem-proving evaluation.
Why it matters
miniF2F became part of the evaluation backbone for formal AI4Math, allowing later systems such as LeanDojo, COPRA and DeepSeek-Prover to report progress against a recognizable shared task.
Significance rationale: miniF2F created a shared set of Olympiad-level statements across formal systems, making progress in neural theorem proving easier to compare and helping establish a durable evaluation target used by later Lean provers.
Historical context
Earlier developments
Later developments
Related milestones
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E3 · Inspectable artifact
- AI role
- Computation only
- Formal assurance
- Artifact available
Contribution & verification
- Mathematical novelty
- Tooling only
- Interface
- Formal, Symbolic
- AI contribution
- AI systems were benchmarked on the dataset, but the benchmark construction and formal statement curation were human-led rather than an AI mathematical discovery.
- Human contribution
- The authors selected source problems, translated and curated formal statements, designed benchmark splits and maintained the cross-system evaluation resource.
- Verification
- Paper released · E3 · Inspectable artifact · Artifact available
- Last reviewed
- 2026-09-11
Technical details
- Systems
- minif2f, lean, metamath, isabelle, hol-light
- Organizations
- openai, formal-mathematics-community
- Problems
- olympiad-mathematics
- Methods
- benchmarking, formalization, theorem-proving
Sources & artifacts
- MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicsS1 · Primary research · Paper · accessed 2026-09-10
- OpenAI miniF2F repositoryS1 · Primary research · Benchmark · accessed 2026-09-10
- miniF2F benchmark repositoryArtifact · Benchmark
Verification history
- 2021-08-31 · Paper released · E2 · Research record
The benchmark was documented in an arXiv paper and released as a public formal-mathematics repository.
Corrections
No corrections recorded.