google-deepmind/miniF2F

google-deepmind/miniF2F

Description: A fork of openai/miniF2F adapted to Lean 4, with corrections to formalizations and informal descriptions. for human readers.

Language: Lean

License: Apache-2.0

Stars: 13

Forks: 3

Open issues: 2

Created: 2025-08-01T18:01:14Z

Pushed: 2026-04-23T14:22:20Z

Default branch: main

Fork: no

Archived: no

README:

MiniF2F


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 Minif2fImport strategy, instead importing all of mathlib.

This is the version of the benchmark on which AlphaProof is evaluated.

This is not an official Google product.