PaperFormalizer transforme les articles LaTeX en code Lean vérifié, avec l'auteur dans la boucle

Une équipe de Stanford propose une méthode destinée à faire de la vérification formelle des articles de mathématiques une étape de routine dans la préparation d'une publication. PaperFormalizer, publié par Jiyuan Tan, Vasilis Syrgkanis et José Blanchet, convertit la source LaTeX d'un article en une version vérifiée par Lean. Il fonctionne comme un pipeline agentique au sein de Claude Code ou Codex. L'idée centrale : même un article soigneusement relu peut contenir de petites lacunes dans les preuves ou dans la formulation des hypothèses, et c'est l'auteur lui-même, aidé par la machine, qui est le mieux placé pour les combler.

Un pipeline de LaTeX à Lean

Le processus part de la source. PaperFormalizer transcrit l'article en un graphe de dépendances entre énoncés : quels lemmes sont nécessaires à quels théorèmes, et qui s'appuie sur quoi. Chaque énoncé fait ensuite l'objet d'un audit en langage naturel selon trois axes : fidélité au sens d'origine, ambiguïté et exactitude. Ce n'est qu'après cette étape que le système formalise les énoncés et les démontre en Lean.

Pour les preuves, le pipeline puise dans plusieurs sources :

• Mathlib, la principale bibliothèque mathématique de Lean ;
• des bibliothèques spécialisées optionnelles, propres à un domaine donné ;
• la boîte à outils personnelle de l'auteur, c'est-à-dire ses propres lemmes et définitions.

Cette boîte à outils s'enrichit au fil du temps. Plus l'auteur fait passer d'articles dans le système, plus il dispose de blocs prêts à l'emploi pour le suivant.

L'auteur décide de ce qu'affirme l'article

L'autoformalisation souffre en général d'un glissement de sens silencieux. Un modèle peut démontrer un théorème formellement irréprochable qui ne dit pas ce que l'auteur voulait dire. Les créateurs de PaperFormalizer partent du principe que seul l'auteur sait ce qu'un énoncé doit signifier et comment combler au mieux une lacune de formalisation.

Le système suit donc plusieurs règles :

• si un énoncé admet plus d'une lecture, le pipeline s'arrête et pose une question ;
• chaque correction est présentée en langage naturel et en symboles TeX comme une proposition que l'auteur peut accepter, rejeter ou rediriger ;
• toute décision susceptible de modifier ce que l'article affirme revient à l'auteur.

À la différence des systèmes qui tentent de formaliser des travaux tiers de manière intégrale et autonome, l'humain joue ici le rôle d'arbitre du sens, tandis que la machine prend en charge la lourde mécanique des preuves.

Ce que l'auteur obtient en sortie

Le résultat comprend trois éléments :

• une version annotée et corrigée de l'article ;
• un rapport de toutes les modifications apportées ;
• du code Lean dans lequel chaque déclaration est liée à l'énoncé qu'elle formalise.

Ce dernier lien compte pour le lecteur. Il peut ouvrir n'importe quel théorème du texte et voir l'objet Lean vérifié qui lui correspond, sans chercher la correspondance à la main.

Une bibliothèque partagée de travaux vérifiés

Les auteurs proposent aussi une couche d'écosystème. Les chercheurs peuvent publier leurs articles vérifiés sur le site paperformalizer.org, et ceux qui construisent sur ces résultats peuvent réutiliser le code Lean existant. Cela réduit le coût de formalisation du travail suivant dans le même domaine : les définitions et lemmes nécessaires existent déjà et sont vérifiés.

L'outil est publié sur GitHub, dans le dépôt Jiyuan-Tan/PaperFormalizer. Le travail est sorti le 22 octobre 2026 et figure dans la sélection quotidienne de Hugging Face Papers ; l'organisation indiquée sur la page est Stanford University.

Quel intérêt concret pour les chercheurs

Pour les mathématiciens et les théoriciens en statistique, en économie et en apprentissage automatique, dont les conclusions reposent sur des preuves, c'est un moyen d'obtenir une vérification indépendante avant l'envoi à une revue. L'outil est particulièrement utile là où des erreurs dans les hypothèses passent la relecture par les pairs sans être détectées. Le seuil d'entrée est plus bas que pour une formalisation manuelle en Lean : il faut la source LaTeX, un accès à Claude Code ou Codex, et la disponibilité pour répondre aux questions du système.

La prudence reste de mise. Le pipeline vérifie que l'énoncé formel est bien démontré, mais c'est toujours un humain qui confirme que la formalisation correspond à l'intention. La qualité du résultat dépend donc de l'attention de l'auteur aux points précis où le système s'arrête pour poser une question.