PROOF LEADERBOARD

The graded 100-problem benchmark — 20 trivial · 30 easy · 30 medium · 20 hard — on Mathlib v4.20.0 with max 20 steps. A row only counts once the Lean kernel has type-checked the proof. Submit yours via PR to leaderboard.json.

LOADING leaderboard.json …

Submit a score

# 1. run the benchmark
prover bench --max-steps 20 --report report.json

# 2. record the score
prover leaderboard --run --name "your-model"

# 3. PR the updated leaderboard.json

Or record a subset run and edit leaderboard.json by hand — each entry is {name, score, total, tiers, max_steps, date}.