A benchmark of graduate-level mathematics problems where models must write Lean 4 proofs that pass formal verification.
114 model results
One row per model and compatible score measure. Mean = equal-weight arithmetic average of imported reports. Distinct configurations reported for the same model in a source table remain separate. Reports can overlap; the range is not a confidence interval. Unbundle to inspect each observation.
#26 of 114 in this displayed comparison; 31 pp below the leader.
Source notes
ProofBench v1.0-era value; model absent from the v1.1 board (vals.ai re-grade 2026-08-14, methodology changed) and not re-run. Not comparable to v1.1 rows. Annotated 2026-08-18.
#38 of 114 in this displayed comparison; 44 pp below the leader.
Source notes
ProofBench v1.0-era value; model absent from the v1.1 board (vals.ai re-grade 2026-08-14, methodology changed) and not re-run. Not comparable to v1.1 rows. Annotated 2026-08-18.
#43 of 114 in this displayed comparison; 46 pp below the leader.
Source notes
ProofBench v1.0-era value; model absent from the v1.1 board (vals.ai re-grade 2026-08-14, methodology changed) and not re-run. Not comparable to v1.1 rows. Annotated 2026-08-18.
#48 of 114 in this displayed comparison; 50 pp below the leader.
Source notes
ProofBench v1.0-era value; model absent from the v1.1 board (vals.ai re-grade 2026-08-14, methodology changed) and not re-run. Not comparable to v1.1 rows. Annotated 2026-08-18.
Epoch AI public data snapshot, CC BY 4.0. Externally collected result; original evaluation provider is linked. CSV: proofbench_external.csv; score column: Accuracy; fraction scale: 1. Model version is retained in configuration. Original source authors retain credit and any additional licensing terms.
ProofBench · Accuracy · 2026-10-26
Public source leaderboard captured 26 October 2026. Model names, configurations, native score units and source-reported uncertainty are retained. Version and task split follow this specific Vals methodology page. These are published observations, not evaluations run by RLTasks.
TRACE THE SCORE · Per-model notes use published breakdowns where available.
Score vs. release date
Epoch AI · 82 observations
ProofBench · Accuracy · % · higher is better
Dates are model release dates recorded by Epoch AI, not evaluation dates. Each point retains its published score and configuration. Separate releases are not a matched longitudinal experiment. Missing dates are omitted. Explore all reported results ↓
The dashed line traces the best observed score through the model release dates. It describes this selection of reports, with their original configurations. It does not estimate unmeasured models or costs.
View plotted values and sources (82)
ProofBench · ProofBench · Accuracy · %. Published measurements in their original score units.
Costs are Vals AI’s published Cost / Test in USD, paired with the score from the same result. They reflect that evaluation’s workload and configuration; they are not token prices or cost per successful task. Missing costs are omitted. Explore all reported results ↓
The dashed line traces the best observed score as reported cost increases. It describes this selection of reports, with their original configurations. It does not estimate unmeasured models or costs.
View plotted values and sources (51)
ProofBench · ProofBench · Accuracy. Published measurements in their original score units.
Epoch AI publishes this benchmark in its capability collection. Imported rows retain the published score column and model configuration. Original authors and evaluation providers remain credited in the result references.
How to read the result
Compare the named task version, tools and scoring rule. Epoch-run evaluations and externally collected results have different provenance. ECI inclusion does not make a benchmark score an ECI value.
Epoch attribution and score coverage
Data is attributed to Epoch AI under CC BY 4.0, with original evaluation providers credited in the linked source snapshots. Scores are imported only where a published mapping identifies the field and its scale; missing or incompatible records are omitted rather than assigned zero.
Versions and evaluation settings
Vals and Epoch point to the same ProofBench leaderboard. Retain source dates, original observations and disclosed conditions.
Where this fits in an evaluation suite
Final-answer accuracy, proof credit, and expert-reviewed research progress are distinct signals. A proof-aware evaluation should retain partial work and audit strong claims.
Start with a capability hypothesis, then choose a second test with a different failure mode. Keep the checkpoint, reasoning effort, agent tools, sampling policy, and scoring procedure fixed when measuring a training intervention. Record failures and missing outputs in the denominator.
A reproducible comparison
Retain Epoch’s task version, source score column, model version, tool setting and sampling budget. External observations retain their original publication URL.
Publish the exact run configuration, item coverage, score units, and available uncertainty. If a source supplies only an aggregate or a single run, preserve that limit. A new model name or a rounded score alone does not establish a capability improvement.