← projects

ten-proofs, faster

Aug 5, 2026

code · math

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. It was also clear from even a cursory glance at the code that there were many inefficiencies and immediate improvements to be made. I figured that for an announcement this important, the Lean code deserved a little extra care to make it more accessible to others.

So, over a couple of days (still ongoing at the time of writing), I made a number of improvements to the codebase and cut the build time by about 40%, down to around ten and a half minutes.

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

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. In reality, 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.

conclusion

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

One day, models will do this work on their own. Until then, there is a great need for Lean experts to clean up AI-generated code so that us humans (and/or future models!) can understand and use them.