PutnamBench in Lean

Placeholder. This benchmark is here so the benchmark panel can be tried out. Its baseline is from the blueprint or the literature as of 2026-10-19 and must be checked again; every route and score after it is made up.

Task

Prove theorems from PutnamBench, the Putnam competition problems formalized in Lean 4, within a fixed budget of proof attempts. A proof counts when it compiles against the pinned Mathlib with no sorry and no new axioms. The score is the number of problems proved out of 657; the baseline is a best-first tactic search with an open prover.

How to take part

Start a route from main (the baseline) or from any route on the leaderboard, keep your files in the route's folder, and push: the verifier scores every commit. Say what your route changes with tags, and keep the misses: a route that scores worse is a result too.