Auto-formalization II: Now What?

In a recent Mastodon post, Terence Tao described the situation with auto-formalization as follows:

In the last few weeks, though, autoformalization has reached the point where virtually every formalization task I had issued could be completed within hours. However, the formalization tools tended to create quite bloated proofs, often hundreds of lines longer than what a human would choose to do, with a lot of redundancy, with many lemmas not stated at the natural level of abstraction.

I share this impression. In a first post I described how I formalized my 2010 paper on binomial edge ideals in Lean 4 over three months with Claude Code. This was completed in May 2026, and the fast-moving world of coding agents has already advanced again. In principle, auto-formalization exists. Even where it does not, working in tandem with coding agents lets one make a lot more progress and drive down the de Bruijn factor.

But then, the standards of the generated code will be low, and most of it will never land in Mathlib (the big Git repository that should contain all “standard” math) and will be hard to reuse. Consequently, all this code likely does not advance the herculean effort of rebuilding the foundations of mathematics in Lean. But it could still be useful if it is out there in Git repositories and, in principle, discoverable (for humans and machines). These repositories could be like obscure publications in unknown or defunct journals that one can still stumble upon today and make something of. Not everything is a 100-times-proofread Annals paper!

Still, having removed many technical barriers, we now face the barriers of social and community organization. How do we make our results useful for a wider community? I think mathematicians have not been the best at this, neither with their papers nor with their computer code. Sure, there are examples of fantastically written papers and beautiful code with tests and documentation, but they are not the standard.

Below I will collect some remaining thoughts on auto-formalization.

Mathlib or It Didn’t Happen

The situation with Mathlib is interesting. On the one hand, it is humming along, well-funded, and we can just wait until the coverage gets better and better. The Cohen–Macaulay results in my formalization are in a pull request already and will land eventually. But then, Mathlib currently has over 2,900 pending pull requests.

Kevin Buzzard, in his post “Accelerating Mathematics,” makes the point that we also can’t speed this up. The bottleneck for formalization (and for extending Mathlib) is the incompleteness of Mathlib itself! Building Mathlib requires people who are simultaneously expert mathematicians, fluent in Lean 4, and (my addition) interested in such an endeavor rather than proving the Riemann hypothesis and becoming famous. Additionally, if you have that skill set, you will get job offers from tech companies.

People say, “Mathlib or it didn’t happen.” Then I guess my BEI-lean project will be in the “didn’t happen” category. One reason is that, as a matter of principle, I don’t send AI-generated stuff to humans to read. I think it’s impolite. But that is just virtue signaling. In reality, I just can’t go through the bureaucratic process of making all this code good. Then I would have to read the LLM output, so I would basically spam myself.

The Monolithic Mathlib

In a recent Quanta article, Mathlib was compared to Bourbaki. I found this very fitting! Even if experts tell me it is no big deal, I’m now very worried: having only one Mathlib (OK, there is also CSLib) is the Lean 4 equivalent of having only one journal in mathematics. And that editorial board would be very powerful in imposing its standards on everything.

In informal math publishing, we have many journals, and they develop their own standards (some better, some worse), but what makes them compatible is the flexibility of being able to cite results from other journals. Experts tell me that Mathlib enforces such strict conditions because the interoperability between different repositories with different conventions would be a new kind of hell. And that also seems plausible.

The Bourbaki comparison is also a bit scary. That group’s austere style marginalized combinatorics and graph theory for decades! Their definitions became canonical not because they were uniquely correct but because they were first and coordinated. A library can do the same: make some mathematics easy and other mathematics awkward, and over time quietly steer what is visible at all.

My paper probably was a good fit for Lean, with a shallow theoretical base and mostly standard commutative algebra and combinatorics. The graph theory, for example, was all there, so in Lean land graph theory is a bit rehabilitated from the pains of the Bourbaki era. In any case, other papers I might have picked would simply not have gone through.

Cost

Fabian Glöckle, a PhD student at Meta, recently deployed roughly 30,000 Claude Opus agents over the course of one week to formalize Darij Grinberg’s textbook An Introduction to Algebraic Combinatorics. This is also largely disjoint from Mathlib, and it does not seem like it would ever be merged, even in part. Most likely, it will end up as one big artifact, roughly ten times the size of the Sphere Packing formalization. The compute cost was on the order of $100,000. Glöckle ran a more expensive experiment than mine (also per page!), but also a more autonomous one under greater time pressure.

Whether LLM costs will go up or down is anyone’s guess. The prices we see today are not real prices. The monthly subscriptions are heavily subsidized, underwritten by investors betting on future revenue rather than charged at cost. For another example, Boris Alexeev is apparently producing on the order of a million lines of Lean on an ordinary Codex subscription.

But then, we also have open-weight models, and we could, in principle, make specialized models for Lean (like Leanstral by Mistral) and power all our data centers with solar energy. If required, we could build a CERN-like organization where scientists organize AI themselves, aligned with their values. I don’t think it is very likely, but in the past there was a time when science convinced the public to use such enormous resources to understand very tiny particles.

In total, cost has to be considered. For comparison, a single open-access publication under the German DEAL agreement costs the taxpayer more than €2,000. The all-in cost of producing one paper in Europe, averaged across the whole research enterprise, is on the order of €70,000. Compared to this, auto-formalization with Claude Code seems cheap.

Definitions Will Be More Important Than Proofs

Tao has his “proof abundance analogy” (see here), which concerns the entire practice of mathematics, but it also concerns auto-formalization: it is much more dangerous to let an LLM write your definition than your proof. The Lean kernel can check that a proof proves the formalized statement, but it can never check that the statement says what you mean. Both in informal and formal mathematics, the proofs could now be the cheap part. The hard, irreducibly human decision is what the objects are, which generality we want, and how to express our ideas. Christian Stump likes to call this “YOU do the math.”

What about the other direction: can you even trust “it compiles”? Not quite beyond all doubt. In an interesting experiment, Tristan Stérin pointed Claude at the kernels of Lean 4 and Rocq and asked it to find soundness bugs: ways to derive a proof of False, from which you can prove anything. Rocq yielded seven. Lean 4’s official kernel gave none, with a single issue that could, in principle, be exploited and was quickly fixed. So the kernel is, at this point, essentially trustworthy. The risk that the compiler was fooled is much smaller than the risk that you formalized the wrong statement.

16/27

Something nice happened after I posted the first post in the series. My former student Tobias Boege asked me if I could spare some tokens and let this run on a problem he and his co-author Ludovick Bouthat had been struggling with. They emailed me the .tex file of an elementary but painful proof: a claim that a certain function on 4 × 4 positive-definite matrices has infimum 16/27. Tobias is an expert in running such things with CAD in Mathematica, but it would not be enough. The informal proof was 17 pages full of many, many by-hand transformations with inequalities. Several pages were completely in red, meaning that the authors did not trust these parts.

I pushed start, and one (!) day later the agent reported back: “Done.” It had not only formalized the proof but also found small gaps in the informal argument and patched them. Apparently, the LLM had learned from the internet that the correct thing in such a situation would be to edit the LaTeX file with blue text, so it also fixed the write-up. Tobias and Ludovick then reworked the argument down to about half its length, and that shorter version was formalized too. It is now on arXiv. I find this uplifting! At very little cost (two days of agent runs), this added real value to research and pushed the project over the finish line.

Conclusion

We are still far from autonomous research. There is no “AI” sitting in the driver’s seat. I view AI as part of the human effort to understand what computers are capable of, and now we marvel at what happens when computers finally learn to do statistics really well. But we should make the decisions. We should reserve the creativity for ourselves and let the computer (coding agents) do the stupid work of checking all the references, typing in all the code, etc. The machine can write the Lean tactics, find gaps, and even shorten the proof. We have to accept that some parts of writing math proofs are just automated statistics, and computers are better at them. In the end, I always enjoyed giving talks more than sitting in my office and trying to find a proof. I think it is important for this new kind of mathematics that there is a human who can give a talk, answer questions, and take responsibility for whatever the machine did.

Mathematics is something that humans use to express their thoughts. That auto-formalization exists now only makes that expression easier and more likely to be correct.