Theorem Proving on PutnamBench Lean
668Solved RateAleph Prover
Evaluation results
| Method | Links | |
|---|---|---|
| Aleph ProverLimit=$1400, Compute Budget=Avg $682026.02 | 668 | |
| Aleph ProverLimit=$400, Compute Budget=Avg $542026.02 | 637 | |
| Seed-Prover 1.5 (ByteDance)Compute Budget=10 H20 days/problem2026.02 | 581 | |
| Aleph ProverLimit=$100, Compute Budget=Avg $232026.02 | 500 | |
| HilbertCompute Budget=avg pass@18402026.02 | 462 | |
| Seed-Prover (ByteDance)Compute Budget=MEDIUM2026.02 | 329 | |
| Ax-ProverCompute Budget=pass@1, avg. 100 tool calls2026.02 | 91 | |
| Goedel-Prover-V2Compute Budget=pass@1842026.02 | 86 | |
| DeepSeek-Prover-V2Compute Budget=pass@10242026.02 | 47 | |
| GPT-5Reasoning=ReAct, Turns=10, Compute Budget=pass@1, 10 tool calls2026.02 | 28 | |
| DSP+Compute Budget=pass@1282026.02 | 23 | |
| BourbakiCompute Budget=pass@5122026.02 | 14 | |
| Kimina-Prover-7B-DistillCompute Budget=pass@1922026.02 | 10 | |
| Self-play Theorem ProverCompute Budget=pass@32002026.02 | 8 | |
| ABELCompute Budget=pass@5962026.02 | 7 | |
| Goedel-Prover-SFTCompute Budget=pass@5122026.02 | 7 | |
| InternLM2.5-StepProverCompute Budget=pass@2x32x6002026.02 | 6 | |
| InternLM 7BCompute Budget=pass@40962026.02 | 4 | |
| gemini-2.5-pro-exp-0325Compute Budget=pass@12026.02 | 3 | |
| gemini-2.0-flash-thinking-121Compute Budget=pass@12026.02 | 1 | |
| Deepseek R1Compute Budget=pass@12026.02 | 1 | |
| COPRABase Model=GPT-4o, Compute Budget=pass@12026.02 | 1 | |
| GPT-4oCompute Budget=pass@102026.02 | 1 |