AI use: none. See the full disclosure (“AI disclosure and licensing”) at the end of this post.
Disclaimer I am a maintainer of Mathlib, the main mathematical library of formalised mathematics in Lean, but all ideas expressed below are my own only; in no way are they supposed to represent an official view of the Mathlib community, nor of its governance.
Introduction
As the mathematical community is swamped by large amounts of results found by different LLMs, we’re reading more and more messages around three main pivots, often intertwined: that “mathematics is truly about understanding”; that those who are the most affected by this revolution are PhD students, or young colleagues in general; and that companies like OpenAI and Anthropic are behaving badly, in one way or another. Somewhat unrelated to the above criticisms, we witness an increasing appearance of the words “formalisation” and, often, “Lean”. I believe that the four strands are related, perhaps in an unexpected way.
The overarching theme around which I’m going to develop my text is that understanding mathematics is a beautiful concept, but very hard to define. At which point can we say that we’ve understood it, and what does it really mean? Can we communicate understanding to colleagues or, even better, to students in a structured way? Can we produce a certificate that some understanding happened? Is there a reproducible outcome of this understanding? To what extent is mathematical understanding a scientific production rather than a method? Is this understanding subject to usual scientific scrutiny? Can we verify it?
I am going to argue that the bare-hand formalisation of mathematics is one answer to the above questions. By formalising mathematics, not only we understand it better but we produce scientific output whose content is precisely this understanding. I will organise this argument by relating what brought me to formalising mathematics six years ago, and why I think that this beautiful human endeavour has very much to do with understanding mathematics, and very little with AI.
A small digression: reasons to worry
Let’s pause for a moment, and look back at the first three points I mentioned above, namely: that mathematics is truly about understanding, that we care about the young generation, that these tech companies’ behaviour is bad and purely driven by economic targets. They remind me of another controversy.
I’ve long been an Open Access advocate, and I’m engaged with some organisations actively promoting it, from MathOA to the French Committee for Open Science. In this role, I’ve often argued that simply accusing the “usual three” Elsevier, Springer, Wiley of being the main obstacle to a full development of open access (in mathematics, or in any other science for that matter) is a red herring: it is our community, so the mathematicians, who put so much emphasis on publications lists and journal rankings. We are those who provide tenure, who promote young colleagues, who refer and distribute grants; and we’re the ones who decide to do so according to the list of shining publications in top (privately owned, often) journals: this approach values understanding very little, rather forcing our young, or less young, colleagues to publish as many papers and as quickly as possible in the top journals in order to obtain full recognition of their hard work. Unfortunately, spending PhD or Postdoc time trying to understand is something that our community has for too long valued way less than publishing in good Elsevier, or Springer, or Wiley journals. We took the easier path of declaring that mathematics was about publishing new results, that the problems came from three bad publishers whom we treated as the beasts, and we’ve refused to change our internal functioning model; yet, it was entirely within our hands.
I’ve heard time and again that we should do something to improve both the “publish or perish” stress imposed on ourselves (and, mostly, over our students’ shoulders), and to take back the power that big publishers can exercise upon our community: nonetheless, little has changed in the last fifteen years. I fear that the same might happen when I read about so many calls to “rethink our profession” in the aftermath of each large release of theorems proved by AIs. But unlike the publishing dead-end where we seem irremediably trapped, we’ve got here a practical action that can be taken: embrace formalisation as a full-fledged mathematical discipline tasked with organising what it means to understand an argument.
Understanding mathematics through its formalisation
To describe how this organisation could develop, let me start by spelling out another point leaving me sceptical at the idea that “mathematics is about understanding”, beyond its vagueness: mathematics cannot be about one thing, simply because it has been studied for more than 2.500 years, by hundreds of thousands of people, and a recent text by Gowers explain this perfectly. In the same vein, I will not dare stating what the true, intrinsic value of formalising mathematics is; but I will try to tell why I consider it a beautiful angle from which to regard mathematics, focusing more on understanding rather than on proving new theorems.
I will not provide any detail about it: I will content myself in saying that formalising mathematics in a proof assistant like Lean, Rocq, Isabelle, HOL-Light, Agda, etc., consists in writing definitions and statements in one of those languages, and then providing the code representing the proofs of the statements. Most of the time, neither of the two can be performed simply by following the informal exposition to be found in articles or monographs. Hence, I should rather say that formalising mathematics consists first in reflecting upon how to write definitions, statements and proofs; and, secondly in writing them down. More often than not, this reflection focuses on mathematical objects that have already been defined somewhere, in some form, and on proofs that already exist; but whose form is unsuited for the formalisation. This unsuitability might amount to inappropriate generality, to verbose computations hiding the core of the idea, to repeated argument hindering the identification of a common pattern. Since the production of new mathematical results is not its substance, the discipline has long faced the question of whether it really was part of mathematics.
When we co-founded, together with my friend and colleague Rob Lewis, the Annals of Formalized Mathematics, we wanted to draft the journal’s Aims and Scope and, helped by the two boards, we wrote, among our criteria, “The act of formalizing mathematics is not mechanical: it involves substantial mathematical insight in its own right, and it constitutes the essence of formalized mathematics”; and “Proof auditing, the act of checking that formal statements correspond correctly to their informal counterparts, is a difficult and inherently human part of reviewing formalized mathematics”. For me, these describe well what constitutes the scientific kernel of the formalisation of mathematics: and explains why it provides an excellent vehicle to communicate and to reason about mathematical understanding. By producing bare-hand formalised artefacts and by writing papers describing what we learn and discover through this activity we are turning understanding into something tangible.
Our formalisation activity typically focuses on looking at an established theorem, or a whole theory, and on trying to distil its understanding to the point where we can sanctify this distillation into a file, or within a whole library. This process I find incredibly pleasant and rewarding, especially because very often this distillation is a community effort: the Mathlib library currently (October 2026) contains two and a half millions of lines of code, written by hundreds of contributors, and it is only as valuable as the existence of the whole Mathlib community around it. We craft, in this manner, a concrete, structured, substantial witness of the community understanding of a topic. It goes without saying that almost every mathematical activity is deeply rooted in understanding, and this is by far not a unique feature of formalisation, nor its defining quality; my point is that the scientific outputs of this activity primarily solidify this understanding, instead of conveying it.
The discovery of this formalisation activity brought me tremendous joy: spending time reading beautiful (even if sometimes horribly written) papers and trying to produce new scientific outputs through their understanding was again my main activity, not an ancillary one that I could try to squeeze in between two attempts at proving my small new theorem. With this perspective, I believe that the production of humanly formalised mathematics in a proof assistant is an excellent way to sail some of the stormy waters we’re encountering: it will assist us in understanding the overabundance of results proven by AI and in creating a transmissible, teachable version of this understanding. As a by-product, it will ensure us that the reasoning beneath those mathematical arguments is sound.
Some thoughts on autoformalisation
I just wrote that getting assurance of the soundness of an argument is a by-product of formalisation. Yet, the pattern we’re observing is rather the following: one or several LLMs are prompted to attack a problem, they do so by producing an argument in the form of a written text and, alongside the text, these agents provide lengthy (Lean, say) code certifying the correctness of their argument. This formalisation performed by an LLM to certify that some argument is correct we call “autoformalisation”. Many colleagues or AI-companies consider this verification the main goal, rather than a by-product, of formalising mathematics in a proof assistant and I respect this position.
But, to my eyes, a huge collection of autoformalised mathematics stands in front of a smaller humanly formalised library like Mathlib as the invention of bookbinding compares to the invention of the press. Bound volumes are the way we experience the usefulness of the press, and they carry its impact in the form of printed pages organised handily and, often, harmonically. Nevertheless, most likely, the refined art of bookbinding would not exist hadn’t Gutenberg’s revolution seen the light of the day. Likewise, when a huge proof—perhaps produced by an LLM, or not—is autoformalised, its correctness is guaranteed (I am aware of technical issues about this guarantee, but let me gloss over them) and this we hold dear. But I look at this autoformalisation as one way of experiencing the usefulness and long-lasting pervasiveness of bare-hand formalisation, carrying its impact to the everyday life of (post?)-modern mathematics. The observation that almost all autoformalisation projects, so far, have been spelling out explicitly that they “rely on Mathlib” is perhaps a sign of such pervasiveness.
Conclusion
I wish more and more colleagues will join our formalisation community, enjoying the beauty of understanding mathematics—whomever or whatever shall it come from—through the painstaking and ever-rewarding activity of formalising it by hand, and discussing their formalisation efforts with even more colleagues and students. The outcomes will take the form of scientific productions contributing to frame the meaning that the broader mathematical community imparts to the idea of understanding, and I hope this might heal our terror that there’s no mathematics ahead of us.
AI disclosure and licensing
No form of AI has been used while producing this text. This text is licensed under a CC-BY 4.0 licence.
Received 15 October 2026.
Add to the discussion