PutnamBench
A multilingual formal theorem-proving benchmark of hand-formalized William Lowell Putnam Mathematical Competition problems in Lean 4, Isabelle, and Coq, where a model's output is scored by whether the proof assistant's compiler verifies the proof.
What this benchmark measures
A multilingual formal theorem-proving benchmark of hand-formalized William Lowell Putnam Mathematical Competition problems in Lean 4, Isabelle, and Coq, where a model's output is scored by whether the proof assistant's compiler verifies the proof.
Rows on this page are sourced from public benchmark artifacts, leaderboard exports, or source-linked model reports. Each row keeps benchmark version, source model name, and available run details attached to the score.
The metric shown here is Problems solved. It should be interpreted within PutnamBench, not compared as part of a site-wide ranking.
Frequently asked
What is PutnamBench?
A multilingual formal theorem-proving benchmark of hand-formalized William Lowell Putnam Mathematical Competition problems in Lean 4, Isabelle, and Coq, where a model's output is scored by whether the proof assistant's compiler verifies the proof. It is a reasoning benchmark measured by Problems solved.
What does Problems solved mean on PutnamBench?
PutnamBench reports Problems solved; higher is better. Scores are shown only within PutnamBench and are never averaged with other benchmarks.
What is the top reported PutnamBench score?
GPT-5 has the top reported score on PutnamBench: 28/660 (Problems solved).
Why do PutnamBench scores differ across runs?
Harness, scaffold, reasoning effort, and prompt setup change results, so two runs of the same model can differ. evals.report keeps each score with its run context so the differences stay visible.
Does evals.report rank models across benchmarks?
No. PutnamBench scores are shown within their own metric; evals.report never combines benchmarks into a composite ranking or a single "best model".