Pour la première fois, l'IA aide à vérifier formellement les preuves d'une médaillée Fields

En mathématiques, il existe une forme de reconnaissance supérieure à toute récompense : qu'un ordinateur confirme que votre preuve est absolument irréprochable. Les preuves de la mathématicienne ukrainienne Maryna Viazovska, qui lui ont valu la médaille Fields en 2022, viennent de passer précisément cette épreuve, avec une participation sans précédent de l'intelligence artificielle.

Viazovska a reçu sa médaille pour avoir résolu l'un des problèmes les plus élégants et les plus retors des mathématiques : l'empilement de sphères. L'énoncé semble simple : comment disposer le plus densément possible des boules identiques dans l'espace ? En deux dimensions, tout apiculteur connaît la réponse : le nid d'abeilles.

En trois dimensions, l'arrangement optimal est la pyramide de boules que connaît quiconque a déjà vu une pile d'oranges sur un étal. Mais à mesure que le nombre de dimensions augmente, le problème devient monstrueusement complexe. En 2016, Viazovska a démontré que la structure symétrique E8 constitue le meilleur empilement en dimension huit et, peu après, avec des collègues, elle a établi que le réseau de Leech est optimal en 24 dimensions.

Aussi abstraits qu'ils paraissent, ces résultats touchent directement aux codes correcteurs d'erreurs qu'utilisent les smartphones et les sondes spatiales.

La communauté mathématique a examiné les preuves et les a jugées correctes, d'où la médaille Fields. Toutefois, la vérification formelle, un processus dans lequel un programme informatique contrôle chaque étape logique de la preuve, relève d'une tout autre échelle. Un relecteur humain peut laisser passer une erreur subtile ; un ordinateur, non. C'est pourquoi la formalisation des preuves complexes est considérée comme l'« étalon-or » de la fiabilité en mathématiques modernes.

Tout a commencé par une rencontre fortuite. À Lausanne, Sidharth Hariharan, étudiant de troisième année, a expliqué à Viazovska comment il utilisait la formalisation de preuves dans le langage Lean pour comprendre en profondeur des concepts mathématiques. Lean est à la fois un langage de programmation et ce qu'on appelle un « assistant de preuve », qui permet d'écrire un raisonnement mathématique sous une forme que l'ordinateur peut vérifier de façon absolument rigoureuse.

Viazovska s'y est intéressée et, en mars 2024, le projet Formalising Sphere Packing in Lean est né. Des experts de l'Imperial College de Londres, de l'université d'East Anglia et de l'université de Californie à Berkeley l'ont rejoint. L'équipe a élaboré un « blueprint », une carte lisible par des humains de tous les éléments de la preuve en dimension huit, indiquant lesquels étaient déjà formalisés et lesquels restaient à traduire en Lean.

Deux ans de travail minutieux ont suivi, puis un tournant. En octobre 2025, la start-up Math, Inc., qui a développé le système d'IA Gauss, a rejoint le projet. Il ne s'agit pas d'un modèle de langage ordinaire : Gauss est un « agent de raisonnement » capable d'alterner raisonnement en langage naturel et déduction mathématique entièrement formalisée. Concrètement, c'est une IA qui sait traduire automatiquement des preuves mathématiques dans un langage que comprend un vérificateur informatique. Gauss a radicalement accéléré la formalisation et a permis d'achever ce qui aurait sinon demandé des années de travail manuel supplémentaires.

Le résultat a eu un fort écho dans la communauté scientifique. « Ces nouveaux résultats paraissent très, très impressionnants et signalent sans conteste un progrès rapide dans cette direction », a déclaré Liam Fowl, chercheur postdoctoral à l'université de Princeton et spécialiste du raisonnement en IA, qui n'a pas participé au projet. Selon lui, la vérification formelle est une sorte de « sceau de qualité », une garantie absolue que chaque étape du raisonnement logique est correcte.

La portée de cette avancée dépasse largement une seule preuve. Jusqu'à récemment, formaliser des résultats mathématiques importants demandait tant de travail que seuls quelques projets isolés s'y attelaient. Si des systèmes d'IA comme Gauss parviennent à accélérer ce travail de façon systématique, les mathématiques obtiendront quelque chose d'inédit : la possibilité de vérifier en masse des preuves accumulées depuis des décennies. Ce n'est pas un remplacement des mathématiciens : Viazovska a bien accompli un exploit intellectuel qu'une machine ne peut pas reproduire. Mais l'IA se révèle indispensable dans la partie la plus routinière et la plus critique du travail : vérifier que l'intuition géniale n'a pas conduit à une erreur dans l'une des milliers d'étapes logiques.

Nous assistons à la naissance d'un nouveau modèle de collaboration : l'humain formule les idées et construit les preuves, la machine garantit qu'elles sont irréprochables. Pour une discipline où une seule erreur passée inaperçue peut jeter le doute sur des décennies de recherches ultérieures, c'est plus qu'un confort : cela change la façon de travailler de la discipline.