evals.report
BenchmarksLabsCompareRun guidesIn the wild
BenchmarksReasoning

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.

ReasoningProblems solvedHigher is better
ScoresAboutRun this benchmark

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. evals.report tracks reported PutnamBench scores with the model, source, status, date, and run caveats attached — official leaderboard scores, vendor-reported launches, and clearly labeled community runs.

Top reported PutnamBench score: GPT-5 — 28/660 (Problems solved).

ModelLabScore↓Source modelStatusDate
GPT-5OpenAI28/660—VerifiedAug 7, 2025Details
Gemini 2.5 ProGoogle DeepMind3—VerifiedMar 25, 2025Details
o4-miniOpenAI2—VerifiedApr 16, 2025Details
GPT-4oOpenAI1—VerifiedMay 13, 2024Details
DeepSeek R1OpenDeepSeek1—VerifiedJan 20, 2025Details
Claude 3.7 SonnetAnthropic0—VerifiedFeb 24, 2025Details
DeepSeek V3 0324OpenDeepSeek0—VerifiedMar 24, 2025Details

Each row reports the model’s Problems solved on PutnamBench. Click a row for the full run context.