State-of-the-Art Formal Theorem Prover
Aleph Prover is a tool that automatically produces machine-checked proofs in Lean 4. On PutnamBench, a collection of problems from the Putnam Competition*, Aleph solved all 672/672 problems (100%), completing the benchmark and placing first among all provers.
*The Putnam Competition is one of the world's most challenging mathematics competitions.
Aleph Prover: 672 / 672 (100%) problems on PutnamBench
First place on leaderboard as of August 25, 2026
Average proof time: ≈ 6h 9m
Average lemmas per proof: ≈ 18
Average cost: ≈ $73.98 per solved problem
Maximum cost: $1,468.74
Notes on This Run
We evaluated Aleph Prover on all 672 problems of PutnamBench. Problems were attempted with an escalating per-problem budget: those not solved within a $100 limit were re-launched with a $300 limit, then with a $1,000 limit, and the last few problems were completed in a final follow-up run with an additional $500 per problem limit. In the end, Aleph solved all 672 of 672 problems (100%). The results were submitted to the PutnamBench authors for verification on August 25, 2026 and published on August 25, 2026.
Fixing Formalization Errors
While working on proofs, Aleph fixed formalization errors in 28 problems. Aleph had access to both the Lean 4 formalization and the original English problem statement. While proving, Aleph identified that the formal statement didn’t match the English problem and proposed corrections. We manually verified each fix, and all 28 corrections were accepted into the official PutnamBench dataset.
All costs reported below include unsuccessful attempts: for each problem, the reported cost is the total amount spent on it across all runs. Problems with fixed formalizations are the exception: their reported costs do not include attempts made before the fix.
About Lean 4
Lean 4 is one of the most popular languages used for machine-checked theorem proving and is the language most widely used by AI tools for automated proving. Unlike proofs written in human languages, Lean 4 allows you to provide the compiler with a formal statement of a theorem and a mathematical proof, and it will automatically verify that the proof is correct or point out errors.
We created Aleph Prover for formal code verification, to provide machine-checked proofs of correctness for code written in any programming language. It has been fine-tuned specifically for proving properties of code. However, it turned out that it also performs very well in solving mathematical competition problems formulated in Lean 4.
While Aleph Prover isn't publicly available yet, we've evaluated it on PutnamBench, a large collection of Lean 4 translations of Putnam competition problems: Aleph solved all 672 of 672 problems, achieving a perfect score on the benchmark.
Putnam Competition
The Putnam Competition (officially the William Lowell Putnam Mathematical Competition) is widely regarded as the most important undergraduate mathematics competition in the United States and Canada. Teams from Harvard and MIT have been among the most successful participants. The authors of PutnamBench emphasize the exceptional difficulty of these problems: "The competition is scored out of 120 points, with the median score typically being zero. The top five individual scorers are named Putnam Fellows, and in recent years regularly include former International Mathematical Olympiad (IMO) medalists."
PutnamBench
A team of researchers from the University of Texas at Austin recently published a paper introducing PutnamBench. The paper describes the manual translation of Putnam competition problems from English into formal languages (including Lean 4). Over many years, statements of 672 problems were translated in this way.
The details about this study can be found at: trishullab.github.io/PutnamBench
Run Statistics
Across all 672 successful proofs, we summarize the distributions for time to proof, lines of Lean code, Lean-check calls, and cost per problem. For transparency, each problem was launched once per run but with many internal Lean checks as needed.
Time Statistics
Lines of Code
Lean Check Calls
Each problem was launched once per run, with many internal Lean-check calls as needed.
Lemmas & Theorems
Each successful proof required on average 18 proved theorems or lemmas, with a minimum of 1 and a maximum of 100. In total 12,119 theorems or lemmas were proved.
Cost Analysis
Per-problem budgets ranged from $100 to $1,000 across runs. Costs include all unsuccessful attempts.
Cost Correlations
Below are charts showing the relationship between cost and time, as well as cost and final code size.
Cost vs Time Correlation
Cost vs Lines of Code