ten-proofs (and zeta-23-lean), faster

Aug 5, 2026 · updated Aug 11, 2026

On August 1, OpenAI released ten-proofs, a collection of Lean files verifying solutions their internal Astra model found to ten previously open problems. Soon after the repository was published, I forked it and tried to build the project myself. Even though I have a pretty decent computer, the build crashed my machine multiple times and took hours before it finally finished. Poking through the code, I could see why: the proofs were full of inefficiencies, many with immediate fixes. I figured that for an announcement this important, the Lean deserved a little extra care to make it more accessible to others.

So, over a couple of days, I chipped away at the codebase and cut the build time by about 40%, down to around ten and a half minutes. (A few days later I did the same thing for Anthropic’s zeta-23-lean; more on that at the end.)

The changes turned out to be pretty simple and unglamorous. I’ll walk through a few of them here.

smaller simp sets

Much of the saved build time came from shrinking simp sets. Calling bare simp in a proof makes Lean match lemmas from the default simp set (of which there are thousands) against every subterm of the goal, over and over until nothing changes. Most proofs only need a handful. Running simp? tells you exactly which lemmas were used, and replacing the call with simp only [...] cuts out the search entirely. There are thousands of simp calls across the ten files, so this accounted for a large chunk of the savings. (Rather than doing this manually, I had a script execute the replacements for me.)

weaker tactics

In the same spirit, the proofs lean (wink wink) heavily on bulky search tactics (nlinarith, aesop, fun_prop, simp_all) where cheaper ones often suffice. For example, nlinarith searches for nonlinear arithmetic certificates even when the goal is linear; often linarith only [h] works, or better, linear_combination. I made similar replacements for aesop and fun_prop.

As an example, a few proofs ended with ring_nf; simp [Complex.I_sq]; ring, normalizing a huge polynomial twice just to substitute $i^2 = -1$ in the middle! A single linear_combination call closes the same goal.

helping out instance search

Some proofs were slow before doing any real work, because Lean was spinning its wheels doing typeclass resolution. If a proof uses a locally finite measure in ten places, Lean may re-derive IsFiniteMeasureOnCompacts from local finiteness ten times. Adding a haveI at the top of the proof pins the instance once, and every step after can use it immediately. Similarly, some lemma applications left implicit arguments uninstantiated, which is expensive when the terms involved are large. Providing them explicitly cuts out more search.

trying rfl first

GapCVP contains a lot of Turing machine step lemmas, all proved by macros that unfold the machine with a big simp call. It turns out most of these lemmas are taken care of by rfl, so wrapping each macro in first | rfl | ... closes them instantly and only falls back to simp when needed.

avoiding giant terms

MetricCodes is a 100,000-line file whose goals contain some very large terms, and several Lean tactics do work proportional to the size of the whole goal rather than just on the part that matters. Some examples: congr 1 on a big sum opens a goal for each piece of the sum, even the side that didn’t change; refine congrArg₂ (· + ·) rfl ?_ only opens one for the summand that did. rw [show a = b from rfl] makes Lean prove that two big terms are definitionally equal and then rewrite with the result, rebuilding the whole goal; when the terms are definitionally equal anyway, show can simply restate the goal directly. Finally, when a general lemma is applied many times with the same large arguments, abstracting into a single helper lemma means Lean only processes the arguments once.

dead code

This was an easy win: tracing the dependencies of each final theorem, I found quite a bit of unused code and other cruft. I deleted the unused definitions and theorems, deduplicated repeated lemmas, and inlined shorthands like def beta (ε : ℝ) : ℝ := ε / 4 which just obfuscate meaning.

zeta-23-lean

A few days after ten-proofs, Anthropic released zeta-23-lean, a formalization of a result about zeros of the Riemann zeta function on the critical line. I forked it here and cut the full build from 6:44 to 4:02 (again about 40%), with theorem statements unchanged and #print axioms still reporting only the usual three.

Most of the wins were the same as above: delete unused code (about 14,000 lines), shrink simp sets, and replace heavy tactics. After those passes, every set_option maxHeartbeats ... override in the library could go; upstream had a lot of them (some set to 1.6M+), and the fork has none.

I also made a few changes specific to this repo: because of the single-theorem and multiple-file structure, I could run shake to remove unused imports, and replace bare import Mathlib with specific modules. This cut even more off of the build time (mostly by allowing for more parallelism).

conclusion

While the Lean in both ten-proofs and zeta-23-lean is certainly correct, the proofs are machine-generated and hard to digest, for both human readers and the compiler. LLMs have gotten extremely good at writing Lean that compiles, but compiling is only the first step: like any other software, code needs to be readable and fast so people can read it, extend it, and build on it.

One day models will do this cleanup themselves. Until then, there is a real need for Lean experts to clean up AI-generated formalizations to make them usable, for both humans and the next model that has to build on them.