Private 100-problem Lean 4 suite: given a natural-language statement and a formal theorem, the model must write a proof the checker accepts.
unassessed
| Category | math |
|---|---|
| Subcategory | Lean 4 graduate-level formal theorem proving |
| Page status | active |
| Metric | proof success rate |
| Direction | higher_is_better |
| Unit | % |
| Dataset size | 100 |
| Publisher | Vals AI |
ProofBench (Vals AI; paper title FormalProofBench) tests whether a model can turn graduate-level math into a machine-checked Lean 4 proof. Each item pairs an English problem with a vetted Lean statement. The model may search Mathlib and run Lean, then must submit one proof. The checker either accepts it or not. There is no partial credit for a plausible write-up. Problems come from qualifying exams and textbooks across analysis, algebra, probability, number theory, and logic, not from contest short-answer keys.
Agentic loop with lean_loogle, lean_run_code, and a single submit_proof. Up to 40 turns (Epoch and Vals write-ups). Natural-language statement plus Lean 4 theorem in; compiled proof out.
No model card in ModelSpec reports this benchmark yet.