Updated daily at 05:00 UTC
Benchmark
ProofBench (Vals AI, FormalProofBench)
Measures: 200 graduate-level problems from qualifying exams and textbooks, each with a Lean 4 statement; the model has 40 turns with Mathlib search and Lean execution and must produce a proof the Lean checker accepts (no partial credit); scored as accuracy.
- Maintainer
- Vals AI
- Introduced
- 2026
- Status
- Active
- Saturation
- Saturated
- Typical provenance
- Independent
- In scoring set
- No
Leaderboard
Every result we hold, whoever ran it. Only independent and third-party rows count towards a score.
No results to show.