ProofBench, created by Vals AI with a team of Lean 4 experts, measures formal theorem proving: each problem pairs a natural-language theorem statement with a vetted Lean 4 formalization, and the model must produce a proof accepted by the Lean 4 checker. Problems are at the graduate or advanced-undergraduate level, spanning analysis, algebra, probability, number theory, and logic. The leaderboard runs on a private 100-problem split, and models work agentically with Mathlib search and code-execution tools over up to 40 turns per problem.

We source results from the public Vals AI ProofBench leaderboard. Our chart reports the proof success rate: the share of problems where the model’s Lean 4 proof passes the formal checker. Scoring is binary per problem with no partial credit, and the leaderboard’s standard error, reasoning-effort setting, latency, and cost per test are kept in the data export.

Because proofs are checked by the Lean 4 compiler rather than a judge, scores reflect fully verified formal correctness. Each model appears once at a fixed reasoning-effort configuration chosen by Vals AI. The leaderboard also includes Harmonic’s Aristotle theorem-proving system, which runs in its own harness and is stored but not charted.