Theorem Proving on ProofNet (test)
21.5Pass Rate (%)DeepSeek-Prover-V1.5-RL + RMaxTS
Evaluation results
| Method | Links | ||||||
|---|---|---|---|---|---|---|---|
| DeepSeek-Prover-V1.5-RL + RMaxTSModel size=7B, Budget=3,2002026.06 | 21.5 | — | — | — | — | — | |
| STP-LeanModel size=7B, Budget=642026.06 | 19.1 | — | — | — | — | — | |
| STP-Lean + OursModel size=7B, Budget=642026.06 | 19 | — | — | — | — | — | |
| STP-Lean + OursModel size=7B, Budget=322026.06 | 18.6 | — | — | — | — | — | |
| DeepSeek-Prover-V1.5 + STP + OursModel size=7B, Budget=642026.06 | 18.5 | — | — | — | — | — | |
| DeepSeek-Prover-V1.5 + STPModel size=7B, Budget=642026.06 | 17.7 | — | — | — | — | — | |
| DeepSeek-Prover-V1.5 + STP + OursModel size=7B, Budget=322026.06 | 17.6 | — | — | — | — | — | |
| DeepSeek-Prover-V1.5-RLModel size=7B, Budget=642026.06 | 17.4 | — | — | — | — | — | |
| STP-LeanModel size=7B, Budget=322026.06 | 17.2 | — | — | — | — | — | |
| DeepSeek-Prover-V1.5 + STPModel size=7B, Budget=322026.06 | 16.8 | — | — | — | — | — | |
| Goedel-Prover-SFTModel size=7B, Budget=642026.06 | 16.7 | — | — | — | — | — | |
| DeepSeek-Prover-V1.5-RLModel size=7B, Budget=322026.06 | 16 | — | — | — | — | — | |
| Goedel-Prover-SFTModel size=7B, Budget=322026.06 | 15.6 | — | — | — | — | — | |
| HAGBPK=64, Search Strategy=best-first search2025.04 | 15.25 | 1.67 | 0.84 | 26.09 | — | — | |
| DeepSeek-Prover-V1.5-SFTModel size=7B, Budget=642026.06 | 15.05 | — | — | — | — | — | |
| HAGBPK=32, Search Strategy=best-first search2025.04 | 14.69 | 1.83 | 1 | 28.57 | — | — | |
| DeepSeek-Prover-V1.5-SFTModel size=7B, Budget=322026.06 | 14.3 | — | — | — | — | — | |
| Hierarchical AttentionK=64, sampling strategy=single-pass2025.04 | 14.12 | 1.8 | 0.75 | 21.74 | — | — | |
| BaselineK=64, sampling strategy=single-pass2025.04 | 13.56 | 2.4 | — | — | — | — | |
| BaselineK=32, Search Strategy=best-first search2025.04 | 13.56 | 1.83 | — | — | — | — | |
| BaselineK=64, Search Strategy=best-first search2025.04 | 13.56 | 2 | — | — | — | — | |
| Hierarchical AttentionK=32, sampling strategy=single-pass2025.04 | 12.8 | 2 | 1 | 31.25 | — | — | |
| BaselineK=16, Search Strategy=best-first search2025.04 | 11.86 | — | — | — | — | — | |
| HAGBPK=16, Search Strategy=best-first search2025.04 | 11.86 | — | — | — | — | — | |
| Hierarchical AttentionK=16, sampling strategy=single-pass2025.04 | 11.3 | — | — | — | — | — | |
| BaselineK=32, sampling strategy=single-pass2025.04 | 10.17 | 2 | — | — | — | — | |
| BaselineK=16, sampling strategy=single-pass2025.04 | 9.6 | — | — | — | — | — | |
| Claude-Opus-4.5Model Category=Close-Weights Reasoning Models2026.03 | — | — | — | — | 35 | — | |
| DeepSeek-Prover-V2-671BModel Category=Open-Weights Prover Models2026.03 | — | — | — | — | 30.5 | — | |
| DeepSeek-Prover-V2-671BBudget (b)=1,0242026.03 | — | — | — | — | — | 37.1 | |
| DeepSeek-Prover-V2-7BModel Category=Open-Weights Prover Models2026.03 | — | — | — | — | 23 | — | |
| DeepSeek-V3.2Model Category=Open-Weights Reasoning Models2026.03 | — | — | — | — | 20.4 | — | |
| Gemini-3 ProModel Category=Close-Weights Reasoning Models2026.03 | — | — | — | — | 22 | — | |
| Goedel-Prover-V2-32BModel Category=Open-Weights Prover Models, Self-correction=false2026.03 | — | — | — | — | 22 | — | |
| Goedel-Prover-V2-8BModel Category=Open-Weights Prover Models, Self-correction=false2026.03 | — | — | — | — | 16.7 | — | |
| Kimi-K2.5Model Category=Open-Weights Reasoning Models2026.03 | — | — | — | — | 19.9 | — | |
| Kimina-Prover-72BModel Category=Open-Weights Prover Models2026.03 | — | — | — | — | 18.3 | — | |
| Kimina-Prover-8BModel Category=Open-Weights Prover Models2026.03 | — | — | — | — | 11.8 | — | |
| Leanabell-Prover-V2-DSModel Category=Open-Weights Prover Models2026.03 | — | — | — | — | 23.7 | — | |
| Leanabell-Prover-V2-DSBudget (b)=1282026.03 | — | — | — | — | — | 25.2 | |
| Leanabell-Prover-V2-KMModel Category=Open-Weights Prover Models2026.03 | — | — | — | — | 13.4 | — | |
| Leanabell-Prover-V2-KMBudget (b)=1282026.03 | — | — | — | — | — | 18.2 | |
| LongCat-Flash-ProverEvaluation Mode=whole-proof mode, TIR (Tool-Integrated Reasoning)=false2026.03 | — | — | — | — | 19.9 | — | |
| LongCat-Flash-ProverEvaluation Mode=whole-proof mode, TIR (Tool-Integrated Reasoning)=true2026.03 | — | — | — | — | 36.1 | — | |
| LongCat-Flash-ProverEvaluation Mode=sketch-proof mode, TIR (Tool-Integrated Reasoning)=true2026.03 | — | — | — | — | 47.3 | — | |
| LongCat-Flash-ProverMode=sketch-proof, Search Strategy=TIR, Budget (b)=682026.03 | — | — | — | — | — | 51.1 | |
| LongCat-Flash-ProverMode=sketch-proof, Search Strategy=TIR & Tree Search, Budget (b)=682026.03 | — | — | — | — | — | 52.2 | |
| Self-play Theorem ProvingBudget (b)=2,5602026.03 | — | — | — | — | — | 26.9 |