This has since moved
The solver later closed the last two: 672 of 672, joint first on the official leaderboard, every proof through Lean 4, Comparator and AXLE. The solver's README has the run.
PutnamBench is 672 formal statements. A Ralph loop running Codex as both worker and reviewer closed 670 of them — 99.7% — including every problem in Putnam 2025.
| Solved | |
|---|---|
| Humanfia — Ralph loop, Codex worker and reviewer | 670 / 672 · 99.7% |
| Logical Intelligence's Aleph, EBM-based | 99.4% |
| Goedel-Architect, autoregressive | 88.8% |
The two that are not closed are not closed. They are drawn as such everywhere we show this.
Where the turns go
More than 90% of problems are solved within ten turns. The loop is not, for most of the benchmark, doing anything exotic — it writes a proof, the compiler objects, it fixes it, and it is done well inside the budget.
The tail is where the argument is. For the harder problems, the extra multi-turn trials raise the solve rate measurably: the same worker, given more rounds against the same feedback, closes problems it did not close in ten. That is the entire thesis of this site stated as an experiment — the model was capable of the proof the whole time, and what was missing was the arrangement that let it keep going without wandering.
Checking it
The official leaderboard is maintained by the PutnamBench team. Proof files are published as a dataset, and a preview set is open for review; the full solving pipeline is public.