Rabdos Lean Bench

Frontier models formalize graduate-level math theorems in Lean, and a semantic, rubric-based checker judges whether the proof actually holds.

Leaderboard

40 problems · Updated Jul 31, 2026

Leaderboard, ranked by average score.
Rank	Provider	Model	Reasoning effort	Graded score	Strict correct
1	Anthropic	Claude Fable 5	max	48.9%	3/40 (7.5%)
2	OpenAI	GPT-5.6 Sol	max	43.6%	2/40 (5.0%)
3	Anthropic	Claude Opus 4.8	max	36.6%	1/40 (2.5%)
4	Moonshot AI	Kimi K3	max	34.6%	1/40 (2.5%)
5	xAI	Grok 4.5	xhigh	25.8%	1/40 (2.5%)
6	Google	Gemini 3.6 Flash	high	22.7%	1/40 (2.5%)
7	Meta	Muse Spark 1.1	xhigh	17.8%	1/40 (2.5%)
8	Z.ai	GLM 5.2	xhigh	14.6%	0/40 (0.0%)
9	DeepSeek	DeepSeek V4 Pro	xhigh	9.4%	1/40 (2.5%)
10	NVIDIA	Nemotron 3 Ultra	high	1.2%	0/40 (0.0%)

Right column: strict correct (of 40)

Sample theorems to formalize

Weyl character triangularity

Representation theory

For any $\lambda \in X(T)_+$ ,

\operatorname{ch} L(\lambda)=e(\lambda)+\sum_{\mu<\lambda}\dim L(\lambda)_\mu\,e(\mu).

Distributional gradients and Hölder regularity

Analysis

Let $u\in\mathcal{D}'(\mathbb{R}^n)$ and assume that $\partial_j u\in L^p(\mathbb{R}^n)$ , $j=1,\ldots,n$ , where $p>n$ . Then $u$ is a continuous function and, with $\gamma=1-n/p$ ,

\sup_{x\ne y}\frac{|u(x)-u(y)|}{|x-y|^\gamma}\le C\sum_j\|\partial_j u\|_p.

Separation by local sampling

Graph theory

Two graph properties $\mathcal{P}_1,\mathcal{P}_2\subseteq\mathcal{G}$ are distinguishable by sampling if and only if $\delta_{\mathcal{G}}(\mathcal{P}_1,\mathcal{P}_2)>0$ .

Interested in evaluating your model on Rabdos Lean Bench? Get in touch →