Browse › Miscellaneous › Automated Theorem Proving › miniF2F-test
miniF2F-test Benchmark (Automated Theorem Proving)
The goal of Automated Theorem Proving is to automatically generate a proof, given a conjecture (the target theorem) and a knowledge base of known facts, all expressed in a formal language. Automated Theorem Proving is useful in a wide range of applications, including the verification and synthesis of software and hardware systems.
Source: Learning to Prove Theorems by Learning to Generate Theorems
The archive carries no text for this table; the description above is the archive's text for the task Automated Theorem Proving. archive 2025-07-28
Over time archive 2025-07-28
The chart needs JavaScript; the table below carries every value.
Not inferred: cumulative, Pass@1, Pass@32, Pass@64, Pass@100, ITP, pass@1024, pass@8192. Points are placed at the row's paper date; 27 of 29 rows carry one.
Results archive 2025-07-28
Archive rows end at the archive snapshot, 2025-07-28: no result published after that date is in this table. Rank is the archive's row order at that snapshot; not re-ranked here. Metric values are the archive's strings. Column headers sort the table in your browser; each row keeps its archive rank.
| Paper | Code | Ran Syntology | Report | ||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 1 | Kimina-Prover-Preview | 80.74 | 52.94 | 68.85 | Lean | 77.87 | 80.74 | ✓ | Paper | Code | 2025 | 3 of 3 ran · 0 unverified | report | ||
| 2 | ProofAug | 66.0 | 36.5 | 52.5 | Isabelle | – | Paper | Code | 2025 | linked, not harvested | report | ||||
| 3 | DeepSeek-Prover-V1.5 | 63.5 | 50.0 | 50.7 | Lean | ✓ | Paper | Code | 2024 | 4 of 10 ran · 6 unverified | report | ||||
| 4 | Subgoal-XL | 56.1 | 39.3 | Isabelle | ✓ | Paper | Code | 2024 | linked, not harvested | report | |||||
| 5 | DeepSeek-Prover | 52.0 | 30.0 | 46.3 | Lean | ✓ | Paper | – | 2024 | no code linked | report | ||||
| 6 | Lyra + GPT-4 | 47.1 | 47.1 | Isabelle | – | Paper | Code | 2023 | 7 of 8 ran · 1 unverified | report | |||||
| 7 | LEGO-Prover ChatGPT | 47.1 | 47.1 | Isabelle | – | Paper | Code | 2023 | linked, not harvested | report | |||||
| 8 | Decomposing the Enigma | 45.5 | 45.5 | Isabelle | – | Paper | Code | 2023 | linked, not harvested | report | |||||
| 9 | Evariste | 41 | 41 | Lean | ✓ | Paper | – | 2022 | no code linked | report | |||||
| 10 | Evariste-7d | 40.6 | 40.6 | Lean | – | Paper | – | 2022 | no code linked | report | |||||
| 11 | Evariste-1d | 38.9 | 38.9 | Lean | – | Paper | – | 2022 | no code linked | report | |||||
| 12 | DSP (540B Minerva informal) | 38.9 | 38.9 | Isabelle | – | Paper | Code | 2022 | linked, not harvested | report | |||||
| 13 | Lean Expert Iteration | 36.6 | 29.6 | 34.5 | 36.6 | Lean | ✓ | Paper | Code | 2022 | linked, not harvested | report | |||
| 14 | GPT-f | 36.6 | 36.6 | Metamath | – | Paper | – | 2022 | no code linked | report | |||||
| 15 | Thor + expert iteration on autoformalised theorems | 35.2 | 35.2 | Isabelle | ✓ | – | – | not matched | report | ||||||
| 16 | COPRA + GPT-4-turbo | 30.7 | 30.7 | Lean | – | Paper | Code | 2023 | linked, not harvested | report | |||||
| 17 | Thor | 29.9 | 29.9 | Isabelle | – | Paper | – | 2022 | no code linked | report | |||||
| 18 | Lean GPT-f | 29.2 | 24.6 | 29.2 | Lean | – | Paper | Code | 2021 | 3 of 3 ran · 0 unverified | report | ||||
| 19 | MMOS-DeepSeekMath-7B | 28.3 | 28.3 | Lean | – | Paper | Code | 2024 | 9 of 11 ran · 2 unverified | report | |||||
| 20 | ReProver | 26.5 | 26.5 | Lean | – | – | – | not matched | report | ||||||
| 21 | LLEMMA-7b | 26.2 | 26.2 | Lean | – | Paper | Code | 2023 | 6 of 8 ran · 2 unverified | report | |||||
| 22 | LLEMMA-34b | 25.8 | 25.8 | Lean | – | Paper | Code | 2023 | 6 of 8 ran · 2 unverified | report | |||||
| 23 | PACT (reproduced by Thor) | 24.6 | 24.6 | Isabelle | – | Paper | Code | 2021 | 3 of 4 ran · 1 unverified | report | |||||
| 24 | COPRA + GPT-4 | 23.3 | 23.3 | Lean | – | Paper | Code | 2023 | linked, not harvested | report | |||||
| 25 | Sledgehammer + heuristics | 20.9 | 20.9 | Isabelle | – | Paper | Code | 2022 | linked, not harvested | report | |||||
| 26 | Lean tidy | 18 | 18 | Lean | – | Paper | Code | 2021 | 3 of 3 ran · 0 unverified | report | |||||
| 27 | COPRA + GPT-3.5 | 11.9 | 11.9 | Lean | – | Paper | Code | 2023 | linked, not harvested | report | |||||
| 28 | Sledgehammer | 10.4 | 10.4 | Isabelle | – | Paper | – | 2022 | no code linked | report | |||||
| 29 | Metamath GPT-f | 1.6 | 1.3 | Metamath | – | Paper | Code | 2021 | 3 of 3 ran · 0 unverified | report |
All 29 rows shown. 27 link to a paper page on this site; 7 are marked as using additional training data in the archive. No GitHub stars are tracked; "Code" is the first repository the archive lists for the row. The archive carries no row tags, review links or community-submitted rows for this table; none are shown. archive 2025-07-28
Syntology Ran reads "N of M ran · U unverified": of the M code samples Syntology harvested from repositories linked to that row's paper (joined by arXiv id), N executed on a synthesized input and the other U = M−N are unverified (harvested, no recorded run). It counts code from repositories linked to that row's paper, not this result: the row's number was not reproduced and nothing here is a correctness claim. The other cell texts mean no graph line for the row: "linked, not harvested" (the archive links code, Syntology has not harvested it), "no code linked" (no code link in the archive), "not matched" (the row's paper URL matched no paper on this site). 10 rows have a graph line, from 7 distinct papers; 10 rows (7 papers) have at least one sample that ran. Counting each paper once: Syntology ran 35 of 47 samples; 12 unverified. Separately, 14 of those 47 are pointer-only (licence): the site points at that code rather than redistributing it, a licence property recorded for ran and unverified samples alike; each cell's tooltip carries the row's own pointer-only count. Read from the graph 2026-09-24. Per-sample status is on the paper page.
Report a problem or propose a change · a person checks every report against the paper or source before anything changes; decisions are listed on /corrections