Annals of Formalized Mathematics : un nouvel épi-journal dédié à la formalisation

Genèse du projet

La formalisation mathématique est un domaine en plein essor et pour lequel il n’y avait pas de revue dédiée. L’idée était de se dire que, parfois, une discipline peut se définir par les journaux qui la représentent : en quelque sorte, ce sont les journaux où sont publiés les articles qui façonnent la discipline. La formalisation mathématique est l’utilisation de certains logiciels pour vérifier des démonstrations mathématiques, on les appelle assistants de preuve. En principe, cette utilisation existe depuis les années 1970 en informatique, mais son utilisation était restée plutôt restreinte jusqu’à très récemment.

Depuis 2016, une communauté grandissante de chercheuses et chercheurs se voue à la formalisation. Mais il nous manquait un journal ! Les pratiques des communautés mathématiques et informatiques en matière de publication sont assez différentes, les mathématiciennes et mathématiciens n’arrivaient pas vraiment à trouver leur compte. Les informaticiennes et informaticiens publient très souvent dans des actes de colloques, congrès, chose qui existe en mathématiques aussi mais est beaucoup moins développée. 

C’était aussi un problème de valorisation de la recherche : on considérait en mathématiques qu’un article publié dans des annales de congrès n’était pas du même niveau qu’un article publié dans une revue. Il était aussi difficile de convaincre les comités éditoriaux informatiques de publier des résultats de formalisation mathématique, où l’accent n’était pas mis sur l’implémentation des logiciels que l’on utilisait mais sur ce que ces logiciels avaient permis d’obtenir d’un point de vue mathématique. Aussi, les actes de colloques imposent souvent une limite aux nombres de pages, tandis que notre objectif était de laisser les autrices et les auteurs choisir sans contraintes leurs niveaux de détail.

Logiciels, assistants de preuves

En 2016, le logiciel Lean a été développé par Microsoft Research tout en restant un logiciel libre. Lean s’est en partie développé à partir de l’expérience Rocq, avant de devenir aujourd’hui un des assistants de preuve les plus utilisés, avec Rocq, Isabelle-HOL et Agda. Bien que la majorité des mathématiciennes et mathématiciens travaillant en formalisation utilisent plutôt Lean, tout article développé dans un de ces langages a sa place au sein des Annals of Formalized Mathematics.

La discipline consiste à trouver la bonne formulation, souvent différente de celle que l’on trouve dans les documents de mathématiques « informelles » pour que le logiciel soit en mesure de comprendre l’énoncé et la démonstration. Si la démonstration qu’on lui fournit n’est pas extrêmement précise, l’ordinateur ne sera pas convaincu. Je trouve cela particulièrement intéressant : il faut souvent changer de langage lorsque l’on utilise ces logiciels, et ce changement de langage est enrichissant, il offre un nouveau regard sur des questions que l’on pensait complètement comprises.

Processus de publication

La revue a été officiellement lancée en avril 2024 après avoir réuni un comité éditorial et un comité scientifique, et en juillet 2025 le premier numéro a été publié. Les articles paraitront ensuite au fil de l’eau. Au départ, nous souhaitions que chaque article soit associé à du code parce que, finalement, formaliser c’est aussi produire des fichiers qui compilent ! L’intérêt aurait été de construire en même temps une collection d’articles scientifiques et d’archives qui puissent à leur tour être réutilisés. En revanche, on s’aperçoit que souvent les manuscrits concernent une contribution à un projet collaboratif : c’est quelque chose que nous n’avions pas anticipé, car il est difficile d’isoler et d’identifier la partie du code qui correspond à la soumission, et en fin des comptes c’est aussi très bien comme ça. Une chose qui nous tient aussi beaucoup à cœur est d’éviter que la revue soit centrée autour de Lean, et plutôt d’offrir une représentation variée des différents assistants de preuve qui existent et sont développés.

Construction d'un épi-journal 

Nous sommes deux co-fondateurs : Robert Y. Lewis de l’Université de Brown à Providence, aux États Unis, et moi-même. Travaillant en France, j’étais déjà familier avec les options qui sont offertes ici pour publier en accès ouvert, surtout en mathématiques. Nous avons donc identifié deux options : Épisciences ou le centre Mersenne. Nous avons opté pour Épisciences, car le modèle de revue que nous avons en tête s’éloigne de celui classique qui est au cœur du travail du centre Mersenne ; nous souhaiterions à terme que le site de la revue donne aussi la possibilité de tester le code directement sur la page de l’article. Nous n’y sommes pas encore là techniquement parlant, mais nous y réfléchissons. Par ailleurs, j’aime beaucoup le modèle des épi-revues, modèle que je trouve sous-représenté. 

Une chose difficile pour beaucoup de comités éditoriaux est de trouver une façon de donner un cadre légal à l’édition de leur revue. En étant aussi dans le comité de direction de MathOA, une structure néerlandaise à but non-lucratif qui s’occupe de l’accès ouvert en mathématiques et qui peut faire office d’éditeur légal, j’ai pu faciliter la création de notre revue par ce biais. 

L’enregistrement du titre à l’Institut National de la Propriété Industrielle (Inpi) nous a coûté 300 euros, et c’est tout ce que nous avons dépensé en frais. Enfin, au moment de la création de notre revue, nous avons eu la chance de bénéficier d’une aide du CCSD pour concevoir une première ébauche de la maquette Latex afin de faciliter la mise en ligne des futurs articles.

Direction et objectifs futurs

L’objectif de la revue est de permettre à plus de chercheuses et chercheurs en mathématiques de partager leurs projets et leurs résultats en formalisation mathématique, de les voir valorisés et d’aider aussi à que ces résultats soient connus au sein de la communauté, même au-delà de la niche qui s’occupe de formalisation. Nous espérons ainsi encourager la reconnaissance de la communauté mathématique envers cette nouvelle discipline. 

Pour terminer en mentionnant la question de l’intelligence artificielle, je dirais qu’il y a sans doute des points de contact entre l’intelligence artificielle pour les mathématiques et la formalisation, mais les deux disciplines restent assez distinctes, chose que nous mentionnons explicitement sur le site de l’AFM. En effet, nous ne considérons pas l’intelligence artificielle comme une thématique pertinente pour les publications de notre revue, qui se concentre plutôt sur les idées mathématiques que l’on obtient, ou les échecs et les écueils, que l’on découvre grâce à l’activité de formalisation.