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
Independent and third-party results only.
No independent or third-party results yet. Show all results