| Paper | Code | Pass@8 | Pass@64 | Pass@1 | Pass@100 | ModelName | ReleaseDate |
|---|---|---|---|---|---|---|---|
| MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics | ✓ Link | 29.3 | 23.9 | Lean GPT-f | 2021-08-31 | ||
| MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics | ✓ Link | 2 | 1 | Metamath GPT-f | 2021-08-31 | ||
| HyperTree Proof Search for Neural Theorem Proving | 58.6 | Evariste | 2022-05-23 | ||||
| HyperTree Proof Search for Neural Theorem Proving | 47.5 | Evariste-7d | 2022-05-23 | ||||
| HyperTree Proof Search for Neural Theorem Proving | 47.3 | GPT-f | 2022-05-23 | ||||
| HyperTree Proof Search for Neural Theorem Proving | 46.7 | Evariste-1d | 2022-05-23 | ||||
| MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics | ✓ Link | 16.8 | Lean tidy | 2021-08-31 | |||
| LEGO-Prover: Neural Theorem Proving with Growing Libraries | ✓ Link | 57.0 | LEGO-Prover ChatGPT | 2023-10-01 | |||
| Lyra: Orchestrating Dual Correction in Automated Theorem Proving | ✓ Link | 52.0 | Lyra + GPT-4 | 2023-09-27 | |||
| Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs | ✓ Link | 43.9 | DSP (62B Minerva informal) | 2022-10-21 |