AI a aidé à vérifier formellement pour la première fois les démonstrations d’une lauréate de la médaille Fields

En mathématiques existe un type spécial de reconnaissance qui dépasse tous les prix : lorsqu'un ordinateur confirme que votre démonstration est absolument impeccable. Les démonstrations de la mathématicienne ukrainienne Marina Viazovska, qui lui ont valu la Médaille Fields en 2022, viennent de passer exactement par une telle vérification — et l'ont fait 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 délicats des mathématiques — le problème d'empaquetage des sphères. Cela semble simple : comment disposer des boules identiques dans l'espace de la manière la plus dense possible ? En deux dimensions, chaque apiculteur connaît la réponse — les rayons de miel.

En trois dimensions, une pyramide de sphères est optimale, familière à quiconque a vu une pile d'oranges sur un étal. Mais à mesure que le nombre de dimensions augmente, le problème devient terriblement complexe. En 2016, Viazovska a prouvé que la structure symétrique E8 est l'empaquetage optimal dans l'espace à huit dimensions, et peu après, avec des collègues, a établi que le réseau de Leech est optimal en 24 dimensions.

Malgré leur apparente abstraction, ces résultats ont une pertinence directe pour les codes correcteurs d'erreurs utilisés par les téléphones intelligents et les sondes spatiales.

La communauté mathématique a vérifié et reconnu les démonstrations comme correctes — d'où la Médaille Fields. Cependant, la vérification formelle — un processus dans lequel chaque étape logique de la démonstration est vérifiée par un programme informatique — est une tâche d'une échelle fondamentalement différente. Un examinateur humain peut passer à côté d'une erreur subtile, un ordinateur ne peut pas. C'est pourquoi la formalisation des démonstrations complexes est considérée comme le « standard d'or » de la certitude en mathématiques modernes.

Tout a commencé par une rencontre fortuite. À Lausanne, un étudiant de troisième année, Siddharth Hariharan, a dit à Viazovska comment il utilisait la formalisation des démonstrations dans le langage Lean pour une compréhension plus profonde des concepts mathématiques. Lean est simultanément un langage de programmation et ce qu'on appelle un « assistant de preuve », permettant d'enregistrer des raisonnements mathématiques sous une forme qu'un ordinateur peut vérifier avec une correction absolue.

Viazovska s'est intéressée, et en mars 2024, le projet Formalising Sphere Packing in Lean est né. Des experts du Imperial College de Londres, de l'Université de East Anglia et de l'Université de Californie à Berkeley s'y sont joints. L'équipe a créé un « plan » — une carte lisible par l'homme de tous les éléments de la démonstration à huit dimensions, indiquant lesquels avaient déjà été formalisés et lesquels devaient encore être traduits en Lean.

Deux ans de travail méticuleux — puis une percée s'est produite. En octobre 2025, la startup Math, Inc., qui a développé le système d'IA Gauss, a rejoint le projet. Ce n'est pas un modèle de langage ordinaire : Gauss est un « agent raisonneur », capable d'alterner entre un raisonnement en langage naturel et une inférence mathématique complètement formalisée. Essentiellement, c'est une IA capable de traduire automatiquement les démonstrations mathématiques en un langage compréhensible pour un vérificateur informatique. Connecter Gauss a accéléré dramatiquement le processus de formalisation, permettant l'achèvement de ce qui aurait autrement pris encore des années de travail manuel.

Le résultat a suscité un écho important dans la communauté scientifique. « Ces nouveaux résultats semblent très et très impressionnants et signalent certainement des progrès rapides dans cette direction », a noté Liam Foul, postdoctorant à l'Université de Princeton et expert en raisonnement par 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.

L'importance de cette percée va bien au-delà d'une seule démonstration. Jusqu'à récemment, la formalisation des résultats mathématiques sérieux était un processus tellement laborieux que seuls des projets isolés s'y aventuraient. Si les systèmes d'IA comme Gauss peuvent systématiquement accélérer ce travail, les mathématiques obtiendront quelque chose de sans précédent : la capacité à vérifier en masse les démonstrations accumulées au fil des décennies. Ce n'est pas un remplacement des mathématiciens — Viazovska a toujours réalisé un exploit intellectuel que les machines ne peuvent pas reproduire. Mais l'IA s'avère indispensable dans la partie la plus routinière et la plus cruciale du travail — vérifier que l'intuition brillante 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 : les humains formulent les idées et construisent les démonstrations, tandis que les machines garantissent leur impeccabilité. Pour les mathématiques, où une erreur négligée peut jeter le doute sur des décennies de recherche ultérieure, ce n'est pas simplement une commodité — c'est un changement de paradigme.