MA-ProofBench - Undergraduate: leaderboard
Metric: Pass@8 (%) on the 100 Level I (undergraduate textbook) theorems, formal Lean 4 theorem proving: the model writes a complete Lean 4 proof of a formalized theorem, accepted only when the Lean compiler verifies it; Pass@8 over sampled proofs (8 for the proprietary models, 32 for the open models, estimated at 8); higher is better. Source: arxiv.org. Saturation forecast: Around 2029. 14 models tracked.
Top models
| # | Model | Score |
|---|---|---|
| 1 | GPT-5.5 (xHigh) | 16 |
| 2 | Gemini 3.1 Pro (Preview) (High) | 13 |
| 3 | Claude Sonnet 4.6 (High) | 6 |
| 4 | DeepSeek V3.2 (Thinking) | 5.56 |
| 5 | nemotron-3-nano-30B-a3B | 3.59 |
| 6 | Qwen 3.5 397B A17B | 3.14 |
| 7 | GPT-OSS-120B (High) | 0.5 |
| 8 | GLM-5.1 | 0.44 |
| 9 | Qwen 3 235B A22B 2507 (Thinking) | 0.25 |
Interactive version: theaggregate.ai/benchmark?slug=ma-proofbench-undergraduate · How It Works · Data refreshed daily, snapshot 2026-09-29.