Independent reproduction of a full PutnamBench solve with open-weight models and a public harness
Difficulty 8: engineering and API spend to rerun a published, public harness; the open questions are run-to-run variance and whether the two DeepSeek V4 snapshots stay available, so it sits at the floor with the other reproduction tasks and far below the FATE-X target (35). Application value 14: it settles whether a cheap, open recipe really saturates competition-level formal proving, which sets expectations for open-weight provers. Leverage 10: it informs how benchmark claims are weighed; little else depends on it.
The problem
Can someone else rerun the public, cheap AI prover that reports solving all 672 Putnam problems in Lean?
- 1Public agent code and open models
- 2Rerun on a pinned PutnamBench commit
- 3Send proofs privately for checking
- 4Compare solved count and cost
Setup. A formal proof is one that the Lean proof checker accepts, and a benchmark is a fixed exam for AI systems. PutnamBench (Tsoukalas et al., 2024) has Lean 4 formalizations of Putnam problems 1962 to 2025: 672 in total, of which 346 require finding an answer. There are separate tracks: with the answer given (the "with solution" track) and without.
The claim. The leaderboard entry "NEAR AI (w/ DeepSeek V4)" reports 672 of 672 with the answer given, at a mean USD 0.17, median USD 0.04, maximum USD 11.18 per problem. It used DeepSeek V4 Flash and V4 Pro open-weight models. The harness is a plain agent loop with a bash tool; the README describes a first pass on V4 Flash (639 solved), a rerun (22 more), then a final run with V4 Pro and a nudge when the agent stops, with the longest problem taking over three days. Two upstream formalizations were defective and were corrected for that run.
Path to understanding
foundations → problemThe research entries this problem rests on, in the order to read them. Each links to its explainer.
- Start with
- Lean 4 & MathlibLibrary
- Step 2
- Machine-assisted theorem provingFrontier
- Step 3
- Then
- Independent reproduction of a full PutnamBench solve with open-weight models and a public harnessThe problem
State of the art
The benchmark is saturated on self-reported results. The leaderboard lists 672 of 672 solved with answers given by Aleph Prover (Logical Intelligence, average USD 74 per problem, 26 August 2026), Humanfia (GPT-5.6, average USD 44.50), NEAR AI (DeepSeek V4, mean USD 0.17) and Forall (Astrio, Claude Opus 5, mean USD 3.52 actor-side cost, closed harness), and 672 of 672 in no-answer mode by Midas Prover (average USD 6.17). Earlier steps: Seed-Prover 1.5 reported 581 in December 2025 at a budget recorded as 10 H20-days per problem (arXiv:2512.17260); Aleph Prover reported 637 and then 668 (December 2025 and January 2026); Mistral's open-weight Leanstral 1.5 reported 587 at about USD 4 per problem (July 2026), and a Mistral scaffold combining DeepSeek V4 Pro with Leanstral reported 658 (September 2026). The NEAR AI entry is the one with a fully public harness and open-weight models; its repository reports 672 validated, namely all 670 solvable upstream problems plus corrected variants of the two whose upstream formalizations were defective. Its total cost was USD 111.85 at the prices of the time; DeepSeek raised prices on 17 August 2026, and the same tokens would now cost a mean of about USD 0.49 per problem at off-peak rates. What is missing is independent confirmation. Several entries are marked as shared privately, the maintainers ask that proofs not be posted publicly (to limit training contamination), and the leaderboard says benchmarked methods were not rerun on problems added after the original release.
Realistic applications
Indirect. A cheap, reproducible recipe for competition-level formal proving is a baseline for AI-assisted formalization at scale and tells the field that this benchmark can be retired as a frontier test.
What counts as solved
An independent team publishes a run log, compute and token cost, the model and harness versions and the pinned PutnamBench, Lean and Mathlib commits, and submits the Lean solutions privately to the PutnamBench maintainers (or a delegated verifier) who confirm the solved count. Success is at least 650 of 672 on statements as they appear at the pinned commit (the two known-defective statements may be handled as the original did, and must be listed), with total token usage within 3 times that of the original run (its costs.tsv lists tokens per run; dollar costs move with API prices), in each of two independent full runs.
How it gets verified
ReproductionA training run, experiment or computation rerun by someone else.
Benchmark: PutnamBench, Lean 4 track, 672 problems, 346 of which require inferring an answer (the track with the answer given is the one reproduced). Pipeline: the harness in nearai/putnambench-deepseek with DeepSeek V4 Flash (0731 snapshot) for the first pass and V4 Pro (0813 snapshot) for the remainder, as the README describes. Metric: number of the 672 problems for which a Lean file is accepted by the kernel against the unmodified statement from the pinned commit; the threshold is at least 650 in each of two independent full runs. Budget: tokens per problem and total API cost reported; total tokens at most 3 times the original run's (the original cost USD 111.85 in total at the prices of the time, a mean of USD 0.17 per problem). Variance: two runs with fresh sessions, since the agent is stochastic and the original needed multiple passes with nudges and a model swap. Verification: solutions are not posted publicly (the maintainers ask that no formal proofs for the benchmark be released in public); they are sent to the maintainers or a delegated verifier, who confirm the count with a kernel check (Comparator or SafeVerify-style) and record the commit used.
Claims under verification
+ add a claimNo claimed results on the Verification board for this problem yet.
Where the work is
Mostly running a published agent at scale and having the results verified; no new mathematics or method.
Bottlenecks
ranked by votes- #1EngineeringVerification channel
Maintainers ask that proofs stay private, so confirmation depends on their capacity to check a bundle.
Community grades
Sign in to add your own grade.
Connected problems
- This problem is related to Half of FATE-X: an open-weight prover solving 50 of 100 PhD-level algebra statements
Progress
- Sep 4, 2026NEAR AI entry with open-weight DeepSeek V4source
672/672 at a mean of USD 0.17 per problem; agent code public, solution bundle shared privately for verification.
- Aug 26, 2026First 672/672 entriessource
Aleph Prover and Humanfia report solving all 672 Lean problems with answers (self-reported).
- Jan 11, 2026Aleph Prover: 668 of 672source
Logical Intelligence's closed system reports 668 (self-reported), after 637 on 26 December 2025.
- Dec 27, 2025Seed-Prover 1.5: 581 of 672source
ByteDance's prover at a budget the leaderboard records as 10 H20-days per problem.