How we achieved #1 on lean-eval in 20 days
lean-eval is the main benchmark of math formalization in Lean. It consists of 128 research-level theorems to prove in Lean 4, and they progressively get harder. Unlike most math benchmarks, it is still far from saturated.
We reached #1 with 92 of 128 problems at the time of writing. We're open-sourcing QuickMaths, our winning harness.
Why not a vanilla harness
In our experiments, a standard harness anchors on the first idea it comes up with. It keeps pushing the route it picked first, even when that route clearly isn't working, and gets stuck in a local minimum.
We built QuickMaths to fix exactly that. We believe a mathematician with this harness will achieve much more than with vanilla Claude, Codex or any other agent. Evolution was a crucial part of our harness. We observed that after each evolution round, a new set of problems closed, and then the solving speed would plateau.
What QuickMaths is made of
1. Distilled methodology from existing research harnesses: our own plus MASS, AdaEvolve and IDS. To distill, we optimize the system in stages (first the role prompts, then how the roles are wired), give compute to the attempts that converge, and pick the highest ROI attempt.
2. Proper infra. Servers, many parallel agent sessions, and a harness with four levels:
- Director manages the whole experiment. It watches how everything runs and how problems get solved, extracts insights, and evolves the harness.
- Orchestrator decides which problem goes into the pool, how many resources it gets and what context to add. It prevents tunnel vision and pushes the Lead out of local minima.
- Lead runs one problem: splits it into blocks, sends out recon, hands off the blocks to the swarm and puts the results together.
- Swarm does the actual proving: each agent takes one block in its own session, writes the proof in Lean, builds it and reports back. Critics check the work.
3. Agents keep their state in a fixed format: what's next, what's still open (with an estimate in lines) and what already failed. So the Orchestrator measures progress instead of asking about it. In successful solving attempts the estimate roughly halved every round, in stuck ones it barely moved round to round.
4. Problems are split into blocks, each tied to a step of the published proof and strictly weaker than the goal. Before anyone proves a block, it is sanity-checked on a concrete example: false intermediate statements were the #1 killer of our long campaigns.
5. Prevention of getting stuck on one idea. This is where a harness beats a single chat:
- Stuck goal. After about 45 minutes on one goal, the agent writes it down and decomposes it again from the statement alone, not from its previous attempts.
- Stalled attempt. The agent reviews its route: marks the current approach as failed, names at least three alternatives from a library of approaches that worked before, and picks the cheapest.
- Fresh context beats repetition. An exact copy of an attempt almost never wins (1 of 17). A restart from the best files in a fresh context wins 10 of 19. Parallel attempts are allowed only on a different route.
- Outside view. When work on a whole problem stops converging, a fresh agent audits it. One audit turned five days on a stuck route into a 9-hour solve.
6. A good validation environment with detailed feedback. We fully replicated the organizers' CI locally, so a problem counts as solved only when it passes the same check they run. A green build or an agent saying "done" doesn't count.
7. Evolution on logs. In our view, the simplest big win, and the reason logging matters so much. We log every trace with metadata, so during the evolve phase the Director finds the specific places where the harness fails and fixes exactly those: it replays our rules on the history, tunes the thresholds and calibrates the agents' estimates. When we noticed the system was getting stuck on one route, we sometimes ran evolve by hand.
8. A solution bank (RAG over useful problems) built from open Lean repositories. By analyzing the patterns in the strongest public proofs, we distilled best practices into the agents' instructions.
9. Our own search for insights over X, arXiv and git. A well-tuned search of our own brings back more useful material than the built-in web search, especially in a niche domain like research-level formalization. We also watch the benchmark's issue tracker: once we spent hours on a problem whose statement had already been disproved there.
10. CI fitting and pep talks. For the last 5 problems we had to step in ourselves: they didn't fit into the CI's 4 CPUs, 15 GB of RAM and 6 hours. So we built an optimization module, local checks, and validation forecasts. We also had to cheer the agent up. On really hard problems it was too pessimistic, got stuck, and kept saying it would need two more weeks. Those forecasts were often wrong, so now measured convergence decides when to stop, not the agent's opinion of its chances.
Try it
The code, the docs and an audit of the campaign are at github.com/genproof/QuickMaths.