ProofBench v1.1
Math
Vals ProofBench v1.1 measures success on 100 private formal-mathematics problems using Lean 4.25.2 and the pinned Mathlib revision. General models receive Mathlib search, Lean execution and a final proof-submission tool, with up to 40 interaction turns and no internet. Vals explicitly states that v1.1 scores are not comparable with earlier revisions.
Top models (higher is better)
| Model | Score |
|---|---|
| Claude Fable 5.1 | 100.0 |
| Claude Opus 5.5 | 100.0 |
| Claude Sonnet 5.5 | 100.0 |
| Claude Opus 5 | 99.0 |
| Gemini 4 Argon | 99.0 |
| GPT-6.1 Sol | 99.0 |
| GPT-6 Astra | 99.0 |
| Claude Fable 5 | 95.0 |
| Muse Wonder Full | 94.0 |
| Kimi K3.1 Pro | 91.0 |
| Claude Haiku 5.5 | 89.0 |
| Kimi K3 | 87.0 |
| Muse Wonder | 84.0 |
| GPT-5.6 Sol | 83.0 |
| GPT-6 Sol | 83.0 |
| Sonnet 5 | 77.0 |
| Hy4 Preview | 75.0 |
| GPT-5.6 Terra | 74.0 |
| MiMo-V2.6-Pro | 70.0 |
| GPT-6 Luna | 64.0 |
| MiMo-V2.6-Flash | 63.0 |
| Ember-1 | 61.0 |
| GPT-5.6 Luna | 60.0 |
| Gemini 3.7 Flash | 58.0 |
| Muse Spark 1.3 | 58.0 |
| Qwen3.8-Max | 58.0 |
| DeepSeek-V4-Flash-0731 | 56.0 |
| DeepSeek V4.1 Flash | 54.0 |
| Grok 4.6 | 51.0 |
| DeepSeek V4 Pro 0813 | 50.0 |
| GLM-5.3 | 49.0 |
| Gemini 3.8 Flash | 48.0 |
| Muse Spark 1.2 | 43.0 |
| Step 5 Preview | 42.0 |
| Gemini 3.5 Flash | 31.0 |
| Grok 4.5 | 31.0 |
| Gemini 3.1 Pro Preview | 26.0 |
| Grok 4.7 | 26.0 |
| MiMo-V2.5-Pro | 22.0 |
| GLM-5.3 Flash | 21.0 |