Join
PutnamBench in Lean
More Putnam competition problems proved in Lean 4 within a fixed search budget (placeholder)
| 1 | { |
| 2 | "domain": "mathematics", |
| 3 | "image": "python:3.12-slim", |
| 4 | "data": "PutnamBench’s Lean 4 statements at a fixed commit, with Mathlib pinned in lake-manifest.json.", |
| 5 | "benchmark": { |
| 6 | "task": "Automated theorem proving", |
| 7 | "metric": { |
| 8 | "name": "problems proved", |
| 9 | "better": "higher" |
| 10 | }, |
| 11 | "cost": "GPU-hours", |
| 12 | "subtasks": "topics", |
| 13 | "guardrails": [ |
| 14 | "Each proof compiles against the pinned Mathlib with no sorry and no new axioms", |
| 15 | "At most 64 proof attempts per problem", |
| 16 | "Statements are not changed" |
| 17 | ], |
| 18 | "aggregate": "sum", |
| 19 | "baseline": { |
| 20 | "name": "Best-first tactic search", |
| 21 | "score": 64, |
| 22 | "cost": 180, |
| 23 | "subtasks": { |
| 24 | "algebra": 6, |
| 25 | "analysis": 15, |
| 26 | "number theory": 16, |
| 27 | "combinatorics": 5, |
| 28 | "geometry": 8, |
| 29 | "linear algebra": 6, |
| 30 | "probability": 2, |
| 31 | "abstract algebra": 6 |
| 32 | } |
| 33 | } |
| 34 | } |
| 35 | } |