MA-ProofBench - Qualifying Exam: leaderboard

Metric: Pass@8 (%) on the 100 Level II (PhD qualifying exam) 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 2030. 14 models tracked.

Top models

#ModelScore
1GPT-5.5 (xHigh)5
2Gemini 3.1 Pro (Preview) (High)5
3Claude Sonnet 4.6 (High)3
4DeepSeek V3.2 (Thinking)1.85
5Qwen 3.5 397B A17B0
6GLM-5.10
7Qwen 3 235B A22B 2507 (Thinking)0
8GPT-OSS-120B (High)0
9nemotron-3-nano-30B-a3B0

Interactive version: theaggregate.ai/benchmark?slug=ma-proofbench-qualifying-exam · How It Works · Data refreshed daily, snapshot 2026-09-29.