(This is a guest post, written by Jeremy Avigad, Kevin Buzzard, Johan Commelin, Rémy Degenne, Kim Morrison, Oliver Nash and Adam Topaz.)
\nMathematicians’ reactions to last week’s big OpenAI release range from excitement to frustration, but one thing is clear: AI has become remarkably good at proving theorems, both formally and informally. The successes in the formal realm have led AI enthusiasts to declare that now is the time to formalize all of mathematics as a legacy for future generations.
\nWe are sympathetic to this proposal. We recognize the power of new technologies for mathematical reasoning and appreciate what they can contribute to the subject we know and love. We are generally optimistic about the role AI can play, but we are deeply concerned by some recent calls to formalize everything as quickly as possible. If done well, a large-scale, coordinated formalization effort could enormously expand mathematical exploration and discovery. Done poorly, it will be, at best, a waste of resources; more likely, it will do lasting damage.
\nWe prefer to see formalization done well. This post therefore clarifies our concerns, describes some of our experiences with AI and formalization, and offers a positive vision of how we can all work toward a world in which all, or almost all, mathematical definitions, theorems, and proofs are equipped with a formal representation, and in which these artifacts help mathematics flourish.
\nJust as the role of AI in mathematics is a fraught subject these days, so too is its role in formalization. The range of attitudes among expert formalizers toward AI is as wide as the range of attitudes among mathematicians more broadly. We are aware that some of our closest friends and colleagues, whose opinions we value and respect highly, stand strongly opposed to large-scale formalization using AI. Nothing we say here should be taken as representative of the views of any of the organizations or communities with which we are associated.
\nLet’s start with the observation that a formal artifact is not worth much if nobody uses it. When Math, Inc. tried to hijack a project to formalize Maryna Viazovska’s higher-dimensional sphere-packing results last February, it impressively demonstrated what the technology could do, but beyond that, it contributed nothing to mathematics. The original project team kept preparing a quality formalization of the 8-dimensional result and soon discovered that cleaning up the AI-generated code was more trouble than it was worth; it turned out it was better to throw the code away and do it right, still with ample help from AI.
\nWhen Anthropic announced that Claude had formally verified Fermat’s Last Theorem with 13 million lines of code written over 11 days, Kevin Buzzard cheerfully lauded the result while also declaring he had no intention of ending his ongoing formalization of a more modern proof. Once again, although the accomplishment is impressive, this piece of AI-generated code probably has little ongoing value.
\nWhat is going on here? The theorems were not seriously in doubt, so the value of the formal artifacts lies solely in what we get beyond mere correctness. We want to formalize everything because we want to use the formalizations to do more mathematics, and to do it better than we could have done without them. We want to think about possible generalizations, explore connections between different branches of mathematics, and consider unexpected applications. We want to refactor and improve our knowledge: part of the joy of manual formalization comes from realizing that we can adjust our concepts to make them more elegant, more efficient, and better suited to our purposes. Knowledge isn’t worth having until it contributes to our understanding; the value of a formalization comes from our ability to use and interact with the data.
\nWhen OpenAI announced solutions to the Navier–Stokes equations that blow up in finite time, the natural-language proof was accompanied by a Lean formalization. In contrast to the previous examples, the correctness signal played a key role here: there seems to be little doubt now that the solution is correct, even though the natural-language proof is mostly incomprehensible. OpenAI nonetheless drew the mathematics community’s anger over concerns about how it obtained the result, provenance and credit for ideas, and worries that focusing on correctness alone discouraged the exploration and understanding the Millenium prize was meant to foster. So, even here, the unadorned formal artifact is a mixed blessing. OpenAI’s later dump contains astonishing and important mathematics, and at the same time shows a remarkable disregard for readers and for building understanding (some results have been retracted, many of the informal/formal pairs diverge in subtle or significant ways, and most of the informal writeups are impenetrable).
\nThis explains our concern. If spending millions of dollars to formalize mathematics results in libraries nobody uses, it will be a terrible waste of resources. Worse, the project could disincentivize good research and productive use of AI, disrupt the social norms and practices research depends on, and set the field back decades. A grand failure will make it hard, or even impossible, to recover later. A lousy formalization of existing results is worse than no formalization at all.
\nSome of the results from the big labs have been done well: OpenAI’s unit distance conjecture work, and Anthropic’s work on the density of Riemann zeta zeroes stand out. They demonstrated impressive new capabilities, contributed to understanding, and the community subsequently built on their work. These are examples of how the labs can contribute positively and we invite further constructive partnerships between the research community and the labs.
\nGood formal libraries will enable the positive vision we have for the future of mathematical research. Humans, AIs, and the Lean language work in concert. Today, AIs are extremely capable in many aspects of mathematical research. Researchers using interactive theorem provers already understand and appreciate the power of having a compiler that can check1 the validity of a proof. Together, these tools are incredibly effective. The AIs will generate formal proofs as they work, constantly checking these against the Lean compiler, and automatically pruning incorrect reasoning. To realize this vision, we will need a high-quality, comprehensive library of formalized mathematics at an unprecedented scale, so mathematicians can work effectively at the frontiers of research. While we are writing as research mathematicians, we must keep in mind that this vision extends beyond mathematics, potentially accelerating research in engineering and science. If and only if we do it right, that payoff would justify a very large investment of resources.
\nWe have argued that if we want to use AI to help with formalization, we need to solve a special case of the alignment problem, namely, ensuring that formal libraries fulfill the community’s mathematical goals. We believe that solving this case will provide powerful lessons about how we can more generally use AI in ways that are safe, reliable, and support our values.
\nHow can we do that? None of us know with certainty: that is part of what makes life on the frontier both exciting and unnerving. But collectively we have experience using AI for formalization, and we should expect any serious effort to pay attention to what we have learned so far. In particular, we want to call attention to the following projects.
\nMathlib is an open-source community-driven library that supports the formal mathematical ecosystem and was awarded the 2026 Jean-Pierre Demailly Prize for Open Science in Mathematics. It is curated by a team of 65 reviewers and 950 contributors to date. Because it emphasizes high-quality, trustworthy code and human curation, Mathlib grows steadily, but more slowly than AI-generated libraries. For the same reasons, it has been the primary place where we learn how to formalize better.
\nFormal Conjectures is a collaborative effort to collect the formal statements of open problems. This is a social enterprise that requires discussion, review, and auditing. AIs can be useful adjuncts, but the goal is to obtain trustworthy statements of the important open questions in various disciplines. We should encourage projects announcing formalizations to use the existing vetted statements of problems wherever possible.
\nThe Annals Challenge. Kevin Buzzard is leading a project to state (but not prove) all the theorems from recent issues of Annals of Mathematics (and later other top journals). The blocker here is missing definitions, and one of the points of the project is that it incentivises good formalizations of definitions which are being used in practice by leaders of the field. Projects like this help us focus effort where it has the highest payoffs.
\nTau Ceti is building a large coherent library of formal mathematics, incubated by the Lean FRO and the Mathlib Initiative. While structurally similar to Mathlib, all contributions are written by AIs, and then adversarially reviewed by other AIs using standard rubrics. These contributions follow roadmaps curated by mathematicians and formalization experts. The review criteria include appropriate generality, avoiding duplication by reusing existing material, documentation, and naming conventions. Tau Ceti extends Mathlib without any duplication, and defers to all design decisions made there. It is possible to contribute to Tau Ceti either by writing roadmaps or by supplying inference2. Tau Ceti is now slightly larger than Mathlib (3 million lines of code), and growing rapidly. Recent results include Riemann-Roch, Schur-Weyl duality, Jordan-Brouwer separation, Rellich-Kondrakov compactness, and Chebotarev density.
\nFormal Frontier is a Mathlib Initiative project building a pipeline converting source texts into interlinked formal libraries. It uses an interacting community of AI agents that can be instructed to formalize specific texts. This system is designed with scalability in mind, so it can ingest thousands of textbooks. There are now 41 released libraries (e.g. on profinite groups, toric ideals, and homological algebra) comprising approximately 200k lines of code. In addition to providing infrastructure to manage the agent swarm, the Formal Frontier project has written a build server for large Lean projects. Recent highlights from Formal Frontier include formalizations of the hairy ball theorem, Kaplansky’s theorem on projective modules, Bass’s stable range theorem, Tate periodicity, and Stone duality for spectral spaces.
\nFormal Frontier and Tau Ceti both use agents and adversarial review, but they differ in their drivers and output structure. Tau Ceti uses roadmaps curated by experts and builds a single coherent library. Formal Frontier is primarily a source-to-library pipeline. Both insist that a formalization is only valuable if others can build on top of it. We anticipate that future autoformalization projects will build upon both approaches.
\nPalomar is an online registry of formal mathematics projects. The goal of Palomar is to index formalization projects aimed at particular results, but not necessarily aspiring to be part of a general library. Many such results have recently been “dumped” on GitHub, and it can be very difficult to interpret or trust them. Palomar addresses this problem by requiring two features in every project it indexes. First, the project must contain a formalization.yaml file, a metadata file containing a self-assessed description of what was formalized, how it was formalized (e.g. solely by humans, in conjunction with AIs, or autonomously by AIs), and also relationships to other work, and how the authors of the underlying informal research were involved in the project. Second, the project must include a Comparator setup, which makes it easier to audit exactly what the statement proves.
Mathlib, Tau Ceti, and Formal Frontier aspire to common values. These are not specific to autoformalization, but rather principles that apply to all formal libraries. The Mathlib community has recently published a document on values, and this is the starting point for our own list.
\nMathlib implements these values through its review process and community discussions. Tau Ceti and Formal Frontier instantiate these values in the code and prompts that drive them, as well as in community-written planning documents.
\nWithin three years, and possibly much sooner, most of mathematics can be formalized in such a way that mathematicians can explore, build on, and make use of formal libraries. This would significantly extend our ability to develop and discover new mathematics. The Lean FRO is committed to ensuring that Lean is able to support projects at this scale. Achieving this ambitious project will require several types of additional support and community participation:
\nAnyone can help build Tau Ceti by running
uv tool install git+https://github.com/TauCetiProject/TauCetiWorker followed by\n tauceti work --loop (You need claude or codex, and the gh GitHub command line tool authenticated.)\n ↩︎