Annals of Formalized Mathematics: a new e-journal dedicated to formalization

Genesis of the project

Mathematical formalization is a rapidly growing field for which there was no dedicated journal. The idea was that, sometimes, a discipline can be defined by the journals that represent it: in a way, it is the journals in which articles are published that shape the discipline. Mathematical formalization is the use of certain software programs to verify mathematical proofs; these are called proof assistants. In principle, this practice has existed in computer science since the 1970s, but its use remained rather limited until very recently.

Since 2016, a growing community of researchers has been devoted to formalization. But we were missing a journal! The publishing practices of the mathematics and computer science communities are quite different, and mathematicians were not really able to find what they were looking for. Computer scientists very often publish in conference proceedings, something that also exists in mathematics but is much less developed.

It was also a problem of research recognition: in mathematics, an article published in conference proceedings was not considered to be of the same level as an article published in a journal. It was also difficult to convince computer science editorial boards to publish the results of mathematical formalization, where the emphasis was not on the implementation of the software being used but on what this software had made it possible to achieve from a mathematical point of view. Furthermore, conference proceedings often impose a limit on the number of pages, whereas our goal was to allow authors to choose their level of detail without constraints.

Software, proof assistants

In 2016, Lean software was developed by Microsoft Research while remaining free software. Lean was developed in part from the Rocq experience, before becoming one of the most widely used proof assistants today, alongside Rocq, Isabelle-HOL, and Agda. Although most mathematicians working in formalization tend to use Lean, any article developed in one of these languages has a place in the Annals of Formalized Mathematics.

The discipline consists of finding the right formulation, often different from that found in “informal” mathematics documents, so that the software is able to understand the statement and the proof. If the proof provided is not extremely precise, the computer will not be convinced. I find this particularly interesting: it is often necessary to change languages when using this software, and this change of language is enriching, offering a new perspective on questions that we thought we had completely understood.

Publication process

The journal was officially launched in April 2024 after an editorial board and scientific committee were assembled, and in July 2025 the first issue was published. Articles will then appear on an ongoing basis. Initially, we wanted each article to be associated with code because, ultimately, formalizing also means producing files that compile! The advantage would have been to build up a collection of scientific articles and archives that could in turn be reused. However, we have found that manuscripts often relate to contributions to collaborative projects. This is something we had not anticipated, as it is difficult to isolate and identify the part of the code that corresponds to the submission, but ultimately, this is fine. Another thing that is very important to us is to avoid focusing the journal solely on Lean, and instead to offer a varied representation of the different proof assistants that exist and are being developed.

Building a journal

There are two co-founders: Robert Y. Lewis from Brown University in Providence, USA, and myself. Working in France, I was already familiar with the options available here for open access publishing, especially in mathematics. We therefore identified two options: Épisciences or the Mersenne Center. We opted for Épisciences because the journal model we have in mind differs from the traditional model that is at the heart of the Mersenne Center's work; ultimately, we would like the journal's website to also offer the possibility of testing the code directly on the article page. We are not there yet technically speaking, but we are thinking about it. Furthermore, I really like the epi-journal model, which I find to be underrepresented.

One thing that is difficult for many editorial boards is finding a way to provide a legal framework for publishing their journal. As I am also on the board of directors of MathOA, a Dutch non-profit organization that deals with open access in mathematics and can act as a legal publisher, I was able to facilitate the creation of our journal in this way.

Registering the title with the Institut National de la Propriété Industrielle (INPI) cost us €300, and that was all we spent in fees. Finally, when we created our journal, we were fortunate to receive assistance from the CCSD in designing a first draft of the Latex template to facilitate the online publication of future articles.

Future direction and objectives

The journal's objective is to enable more mathematics researchers to share their projects and results in mathematical formalization, to see them promoted, and to help make these results known within the community, even beyond the niche that deals with formalization. We hope to encourage the mathematics community's recognition of this new discipline.

To conclude by mentioning the question of artificial intelligence, I would say that there are undoubtedly points of contact between artificial intelligence for mathematics and formalization, but the two disciplines remain quite distinct, something we mention explicitly on the AFM website. In fact, we do not consider artificial intelligence to be a relevant topic for our journal's publications, which focus instead on the mathematical ideas that are obtained, or the failures and pitfalls that are discovered, through the activity of formalization.