Automated Theorem Proving on miniF2F-test
Metric: Pass@32 (higher is better)
Metric: Pass@32 (higher is better)
| # | Model↕ | Pass@32▼ | Extra Data | Paper | Date↕ | Code |
|---|---|---|---|---|---|---|
| 1 | Kimina-Prover-Preview | 68.85 | Yes | Kimina-Prover Preview: Towards Large Formal Reas... | 2025-04-15 | Code |
| 2 | DeepSeek-Prover-V1.5 | 50 | Yes | DeepSeek-Prover-V1.5: Harnessing Proof Assistant... | 2024-08-15 | Code |
| 3 | Subgoal-XL | 39.3 | Yes | SubgoalXL: Subgoal-based Expert Learning for The... | 2024-08-20 | Code |
| 4 | Lean Expert Iteration | 34.5 | Yes | Formal Mathematics Statement Curriculum Learning | 2022-02-03 | Code |
| 5 | Lean GPT-f | 29.2 | No | MiniF2F: a cross-system benchmark for formal Oly... | 2021-08-31 | Code |
| 6 | ReProver | 26.5 | No | - | - | - |
| 7 | LLEMMA-7b | 26.2 | No | Llemma: An Open Language Model For Mathematics | 2023-10-16 | Code |
| 8 | LLEMMA-34b | 25.8 | No | Llemma: An Open Language Model For Mathematics | 2023-10-16 | Code |