Formal Theorem Proving on PutnamBench
668Solved CountALEPH
Evaluation results
| Method | Links | ||
|---|---|---|---|
| ALEPHSize=?, Budget=$14002026.03 | 668 | — | |
| ALEPHSize=?, Budget=$4002026.03 | 637 | — | |
| SEED-V1.5*Size=?, Budget=10H 20DAYS2026.03 | 581 | — | |
| Seed-Prover 1.5Compute Budget=10 H20 days / problem2025.12 | 580 | 87.9 | |
| ALEPHSize=?, Budget=$1002026.03 | 500 | — | |
| HILBERT*Size=?, Budget=18402026.03 | 462 | — | |
| SEED*Size=?, Budget=MEDIUM2026.03 | 329 | — | |
| Goedel-32BSize=32B, Budget=2562026.03 | 110 | — | |
| GOEDEL VALUESampling Budget=256, Search Strategy=Value-guided tree search2026.03 | 110 | — | |
| GOEDEL RANDOMSampling Budget=256, Search Strategy=Random search2026.03 | 104 | — | |
| Pythagoras-ProverOpen-source=true, Compute=pass@20482026.06 | 93 | — | |
| AX-PROVER*Size=≥ 72B, Budget=100 TOOLS2026.03 | 91 | — | |
| GOEDEL-V2*Size=32B, Budget=1842026.03 | 86 | — | |
| Goedel-Prover-V2 (self-correction mode)Open-source=true, Compute=pass@1842026.06 | 86 | — | |
| GOEDEL VALUESampling Budget=128, Search Strategy=Value-guided tree search2026.03 | 82 | — | |
| GOEDEL RANDOMSampling Budget=128, Search Strategy=Random search2026.03 | 80 | — | |
| GOEDEL RANDOMSampling Budget=64, Search Strategy=Random search2026.03 | 63 | — | |
| GOEDEL VALUESampling Budget=64, Search Strategy=Value-guided tree search2026.03 | 63 | — | |
| Pythagoras-ProverOpen-source=true, Compute=pass@642026.06 | 59 | — | |
| Goedel-Prover-V2 (self-correction mode)Open-source=true, Compute=pass@322026.06 | 57 | — | |
| Pythagoras-ProverOpen-source=true, Compute=pass@322026.06 | 48 | — | |
| DSP-V2Size=671B, Budget=10242026.03 | 47 | — | |
| DeepSeek-Prover-V2Open-source=true, Compute=pass@10242026.06 | 47 | — | |
| GOEDEL DIRECTSampling Budget=256, Supervision Strategy=direct synthesis2026.03 | 44 | — | |
| Goedel-Prover-V2Open-source=true, Compute=pass@322026.06 | 43 | — | |
| GOEDEL-V2Sampling Budget=2562026.03 | 41 | — | |
| GOEDEL-V2Sampling Budget=1282026.03 | 38 | — | |
| GOEDEL DIRECTSampling Budget=128, Supervision Strategy=direct synthesis2026.03 | 37 | — | |
| GOEDEL-V2Sampling Budget=642026.03 | 32 | — | |
| GPT-5*Size=?, Budget=10 TOOLS2026.03 | 28 | — | |
| GOEDEL DIRECTSampling Budget=64, Supervision Strategy=direct synthesis2026.03 | 28 | — | |
| Kimina-8BSize=8B, Budget=2562026.03 | 25 | — | |
| KIMINA VALUESampling Budget=256, Search Strategy=Value-guided tree search2026.03 | 25 | — | |
| DSP+*Size=≥ 32B, Budget=1282026.03 | 23 | — | |
| KIMINA VALUESampling Budget=128, Search Strategy=Value-guided tree search2026.03 | 23 | — | |
| DSP+Open-source=true, Compute=pass@1282026.06 | 23 | — | |
| DeepSeek-Prover-V2Open-source=true, Compute=pass@322026.06 | 22 | — | |
| KIMINA RANDOMSampling Budget=256, Search Strategy=Random search2026.03 | 21 | — | |
| KIMINA RANDOMSampling Budget=128, Search Strategy=Random search2026.03 | 20 | — | |
| KIMINA VALUESampling Budget=64, Search Strategy=Value-guided tree search2026.03 | 20 | — | |
| KIMINA RANDOMSampling Budget=64, Search Strategy=Random search2026.03 | 17 | — | |
| KIMINA DIRECTSampling Budget=256, Supervision Strategy=direct synthesis2026.03 | 16 | — | |
| BOURBAKISize=7B, Budget=5122026.03 | 14 | — | |
| KIMINA DIRECTSampling Budget=128, Supervision Strategy=direct synthesis2026.03 | 14 | — | |
| BourbakiOpen-source=true, Compute=pass@5122026.06 | 14 | — | |
| KIMINA DIRECTSampling Budget=64, Supervision Strategy=direct synthesis2026.03 | 12 | — | |
| KIMINASize=8B, Budget=1922026.03 | 10 | — | |
| KIMINASampling Budget=642026.03 | 10 | — | |
| KIMINASampling Budget=1282026.03 | 10 | — | |
| KIMINASampling Budget=2562026.03 | 10 | — | |
| Kimina-Prover-7B-DistillOpen-source=true, Compute=pass@1922026.06 | 10 | — | |
| STPSize=7B, Budget=32002026.03 | 8 | — | |
| Self-play Theorem ProverOpen-source=true, Compute=pass@32002026.06 | 8 | — | |
| GOEDEL-V1Size=7B, Budget=5122026.03 | 7 | — | |
| Goedel-Prover-SFTOpen-source=true, Compute=pass@5122026.06 | 7 | — | |
| ABELOpen-source=false, Compute=pass@5962026.06 | 7 | — | |
| Aleph ProverCompute Budget=avg 1834 tool calls2025.12 | — | 75.8 | |
| AlphaProofCompute Budget=500 TPU days / problem2025.12 | — | 56.1 | |
| Ax-Proverpass@k=pass@12026.02 | — | 13.8 | |
| AxProverBaseunderlying LLM=Opus 4.5, thinking budget=32k, iterations=50, pass@k=pass@12026.02 | — | 54.7 | |
| AxProverBaseNumber of samples (k)=12026.06 | — | 54.7 | |
| DeepSeek V2pass@k=pass@10242026.02 | — | 7.1 | |
| DeepSeek-Prover-V2-7B2025.10 | — | 22 | |
| GAR DeepSeek-Prover2025.10 | — | 24 | |
| Goedel Prover V2pass@k=pass@1842026.02 | — | 13 | |
| Goedel-ArchitectNumber of samples (k)=1, Natural language guidance (+NL)=false2026.06 | — | 75.6 | |
| Goedel-ArchitectNumber of samples (k)=4, Natural language guidance (+NL)=true2026.06 | — | 88.8 | |
| Goedel-Prover-V2Number of samples (k)=1842026.06 | — | 13 | |
| HilbertCompute Budget=avg pass@18402025.12 | — | 70 | |
| Hilbertpass@k=pass@18402026.02 | — | 70 | |
| HilbertNumber of samples (k)=18402026.06 | — | 70 | |
| Kimina Proverpass@k=pass@1922026.02 | — | 1.5 | |
| LongCat-Flash-ProverNumber of samples (k)=1182026.06 | — | 41.5 | |
| Seed-Prover2026.06 | — | 50.4 | |
| Seed-Prover 1.0 (medium)Compute Budget=18 H20 days / problem2025.12 | — | 50.4 | |
| Seed-Prover 1.52026.02 | — | 87.9 | |
| Seed-Prover 1.52026.06 | — | 87.9 |