ProofBench
Math · 2026-03-27
Automated theorem-proving benchmark for formal mathematical proof tasks. Scores measure the share of proof obligations solved.
Top models (higher is better)
| Model | Score |
|---|---|
| Claude Opus 5 | 78.0 |
| Claude Fable 5 | 77.0 |
| GPT-5.6 Sol | 77.0 |
| Aristotle | 71.0 |
| GPT-5.6 Terra | 71.0 |
| Kimi K3 | 70.0 |
| Opus 4.8 | 69.0 |
| Sonnet 5 | 66.0 |
| GPT-5.4 | 56.0 |
| Opus 4.7 | 54.0 |
| GPT-5.6 Luna | 54.0 |
| Opus 4.6 | 50.0 |
| GPT-5.5 | 50.0 |
| Sonnet 4.6 | 45.0 |
| Muse Spark 1.1 | 39.0 |
| Opus 4.5 | 36.0 |
| Gemini 3.6 Flash | 36.0 |
| GLM-5.2 | 35.0 |
| Grok 4.5 | 30.0 |
| Gemini 3.5 Flash | 29.0 |
| Gemini 3.1 Pro Preview | 26.0 |
| Qwen3.7-Max | 26.0 |
| MiMo-V2.5-Pro | 24.0 |
| GLM-5.1 | 22.2 |
| GPT-5.4 Mini | 21.0 |
| Gemini 3 Pro Preview | 20.0 |
| Sonnet 4.5 | 19.0 |
| MiniMax M3 | 19.0 |
| GPT-5 | 18.0 |
| Muse Spark | 17.0 |
| Kimi K2.6 | 16.0 |
| MiMo-V2.5 | 16.0 |
| Gemini 3 Flash Preview | 15.0 |
| GPT-5.2 | 15.0 |
| Grok 4.20 | 14.0 |
| Gemini 3.5 Flash-Lite | 13.0 |
| GPT-5 Nano | 12.0 |
| Grok 4.3 | 11.0 |
| DeepSeek-V4-Pro | 10.0 |
| Mistral Medium 3.5 | 10.0 |