Formal Theorem Proving on ProofNet (test)
44.62Pass@1ProofSketcher
Evaluation results
| Method | Links | |||
|---|---|---|---|---|
| ProofSketcher2026.04 | 44.62 | — | — | |
| DeepSeek-Prover-V22026.04 | 37.1 | — | — | |
| GAR on Deepseek-Prover-V2Sample budget=322025.10 | 25.81 | — | — | |
| DeepSeek-Prover-V2-7BSample budget=322025.10 | 22.58 | — | — | |
| STP-LeanSample budget=1282025.10 | 19.5 | — | — | |
| InternLM-2.5-StepProverSample budget=4 × 32 × 6002025.10 | 18.8 | — | — | |
| DeepSeek-Prover-V1.5-RLSample budget=1282025.10 | 18.2 | — | — | |
| MA-LoTSample budget=322025.10 | 15.47 | — | — | |
| ReProver*Model detail=newly provided pre-trained model2025.03 | 15.3 | — | — | |
| LeanListener2025.03 | 14.4 | — | — | |
| ReProver (LeanDojo)2026.04 | 13.98 | — | — | |
| ReProver2025.03 | 13.8 | — | — | |
| DeepSeek-Prover-V1.5-BaseSample budget=32002024.08 | — | 15.6 | — | |
| DeepSeek-Prover-V1.5-RLSample budget=4 x 64002024.08 | — | 23.7 | — | |
| DeepSeek-Prover-V1.5-RL + RMaxTSSample budget=4 x 64002024.08 | — | 25.3 | — | |
| DeepSeek-Prover-V1.5-SFTSample budget=4 x 64002024.08 | — | 23.7 | — | |
| DeepSeek-Prover-V1.5-SFT + RMaxTSSample budget=4 x 64002024.08 | — | 25.8 | — | |
| DeepSeek-Prover-V2-7BBudget=322026.05 | — | — | 21.9 | |
| DeepSeek-Prover-V2-7BBudget=642026.05 | — | — | 23.1 | |
| DeepSeek-Prover-V2-7B + EnsembleBudget=322026.05 | — | — | 21.9 | |
| DeepSeek-Prover-V2-7B + EnsembleBudget=642026.05 | — | — | 23.2 | |
| Goedel-Prover-DPOBudget=322026.05 | — | — | 13.6 | |
| Goedel-Prover-DPOBudget=642026.05 | — | — | 14.5 | |
| Goedel-Prover-DPO + EnsembleBudget=322026.05 | — | — | 15.6 | |
| Goedel-Prover-DPO + EnsembleBudget=642026.05 | — | — | 16.8 |