Benchmark · math

PutnamBench

2 results 1 models

PutnamBench is a formal theorem-proving benchmark built from undergraduate competition mathematics: it measures how many Putnam Competition problems a system can prove inside a proof assistant (Lean 4, Isabelle, or Coq), scored as the count or fraction of machine-verified proofs.

Example: A hard undergraduate Putnam problem — such as a number-theory divisibility claim, a bound on an integral or inequality, or a combinatorial identity — presented as a formal theorem statement whose proof is left as `sorry` for the system to fill in.
Scoring: The metric is the number (or percentage) of problems for which the system produces a complete formal proof. A problem counts only if the proof assistant fully verifies it; partial arguments or informal reasoning score zero.
Verification: A result is accepted only when the target proof assistant's kernel type-checks the entire proof with no `sorry`, no extra axioms, and no change to the given statement — the verifier's yes/no is the only judge.
Why it matters: Putnam problems are among the hardest undergraduate mathematics, and machine-checked proofs leave no room for incorrect or reward-hacked reasoning, making PutnamBench a rigorous and much harder successor to MiniF2F for automated theorem proving and mathematical reasoning.

Worked example

Task

(Illustrative, simplified.) A Lean 4 theorem in the PutnamBench format, to be proved with no sorry: ```lean theorem putnam_illustrative (n : ℕ) : ∑ i ∈ Finset.range n, (2 * i + 1) = n ^ 2 := by sorry ```

Solution

```lean
theorem putnam_illustrative (n : ℕ) :
    ∑ i ∈ Finset.range n, (2 * i + 1) = n ^ 2 := by
  induction n with
  | zero => simp
  | succ k ih => rw [Finset.sum_range_succ, ih]; ring
```

Walkthrough

The sum of the first n odd numbers equals n^2, proved by induction: the base case reduces to 0 = 0, and the step uses Finset.sum_range_succ, applies the induction hypothesis, and closes k^2 + (2k+1) = (k+1)^2 with ring. It passes only because Lean's kernel accepts every step — a genuine PutnamBench item is far harder.

Leanstral 1.5

Timeline

Date	Model	Score	Source
2026-07-03	Leanstral 1.5	587.0pts	Mistral released Leanstral-1.5-119B-A6B
2026-07-03	Leanstral 1.5	587.0pts	Leanstral 1.5: Proof Abundance for All