Theorem Proving on PutnamBench Lean 4 (full)
668Solved CountAleph ($1400 cap)
Evaluation results
| Method | Links | |||
|---|---|---|---|---|
| Aleph ($1400 cap)Backbone=GPT-5.2 agentic, Setting=Pass@32026.06 | 668 | 99.4 | 68 | |
| Aleph ($400 cap)Backbone=GPT-5.2 agentic, Setting=Pass@22026.06 | 637 | 94.8 | 54 | |
| Seed-Prover 1.5Backbone=10 H20-GPU-day budget per problem2026.06 | 581 | 86.5 | 168 | |
| Aleph ($100 cap)Backbone=GPT-5.2 agentic, Setting=avg. 1,834 tool calls2026.06 | 500 | 74.4 | 23 | |
| HilbertBackbone=Gemini 2.5 Pro + Goedel-V22026.06 | 462 | 68.8 | 39 | |
| AxProverBaseBackbone=Claude Opus 4.5, Setting=50 tool calls2026.06 | 365 | 54.3 | 12.6 | |
| Seed-ProverBackbone=RL-tuned, Setting=“medium” compute2026.06 | 329 | 49 | — | |
| Goedel-Prover-V2Backbone=32B, Setting=Pass@184 + self-correct2026.06 | 86 | 12.8 | 1 | |
| DeepSeek-Prover-V2Backbone=671B MoE (37B active), Setting=Pass@10242026.06 | 47 | 7 | 18 | |
| GPT-5 (ReAct, 10 turns)Backbone=GPT-5, Setting=Pass@1, ≤ 10 tool calls2026.06 | 28 | 4.2 | 1 | |
| BourbakiBackbone=7B, Setting=Pass@5122026.06 | 26 | 3.8 | 1 | |
| Kimina-Prover-7B-DistillBackbone=7B, Setting=Pass@1922026.06 | 10 | 1.5 | 1 |