Un moment décisif pour la collaboration entre l'IA et les humains en mathématiques

Un moment décisif pour la collaboration entre l'IA et les humains en mathématiques

Lorsque la mathématicienne ukrainienne Maryna Viazovska a reçu une Médaille Fields—largement considérée comme le prix Nobel des mathématiques—en juillet 2022, cela a fait grand bruit. Non seulement elle était la deuxième femme à recevoir cet honneur en 86 ans d'histoire de l'attribution, mais elle a reçu la médaille quelques mois après l'invasion de son pays par la Russie. Près de quatre ans plus tard, Viazovska fait à nouveau parler d'elle. Aujourd'hui, grâce à une collaboration entre humains et IA, les preuves de Viazovska ont été formellement vérifiées, signalant un progrès rapide dans les capacités de l'IA à assister la recherche mathématique. “Ces nouveaux résultats semblent très, très impressionnants et signalent définitivement un progrès rapide dans cette direction,” déclare Liam Fowl, expert en raisonnement IA et postdoctorant à l'Université de Princeton, qui n'a pas participé à ce travail.

Dans ses recherches récompensées par la Médaille Fields, Viazovska a abordé deux versions du problème de l'empilement de sphères, qui pose la question suivante : comment des cercles, sphères, etc., identiques peuvent-ils être empilés de manière aussi dense que possible dans un espace n-dimensionnel ? En deux dimensions, la meilleure solution est le nid d'abeille. En trois dimensions, les sphères empilées en pyramide sont optimales. Mais après cela, il devient extrêmement difficile de trouver la meilleure solution et de prouver qu'elle est effectivement la meilleure. En 2016, Viazovska a résolu le problème dans deux cas. En utilisant des fonctions mathématiques puissantes connues sous le nom de formes (quasi-)modulaires, elle a prouvé qu'un arrangement symétrique appelé E8 est le meilleur empilement en 8 dimensions, et peu après, elle a prouvé avec des collaborateurs qu'un autre empilement de sphères appelé réseau de Leech est le meilleur en 24 dimensions. Bien que cela semble abstrait, ce résultat a le potentiel d'aider à résoudre des problèmes quotidiens liés à l'empilement dense de sphères, y compris les codes de correction d'erreurs utilisés par les smartphones et les sondes spatiales.

Les preuves ont été vérifiées par la communauté mathématique et jugées correctes, ce qui a conduit à la reconnaissance par la Médaille Fields. Mais la vérification formelle—la capacité d'une preuve à être vérifiée par un ordinateur—est une tout autre affaire. Depuis 2022, de nombreux progrès ont été réalisés dans la vérification formelle assistée par IA.

Une rencontre fortuite relance l'intérêt

Quelques années plus tard, une rencontre fortuite à Lausanne, en Suisse, entre l'étudiant de troisième année Sidharth Hariharan et Viazovska raviverait son intérêt pour les preuves d'empilement de sphères. Bien qu'il soit encore très tôt dans sa carrière, Hariharan devenait déjà habile à formaliser des preuves.

“La vérification formelle d'une preuve est comme un tampon en caoutchouc,” explique Fowl. “C'est une sorte de certification authentique que vous savez que vos énoncés de raisonnement sont corrects.” Hariharan a expliqué à Viazovska comment il avait utilisé le processus de formalisation des preuves pour apprendre et vraiment comprendre des concepts mathématiques. En réponse, Viazovska a exprimé un intérêt pour la formalisation de ses preuves, principalement par curiosité. De cette interaction est né, en mars 2024, le projet Formalising Sphere Packing in Lean. Lean est un langage de programmation populaire et un “assistant de preuve” qui permet aux mathématiciens d'écrire des preuves qui sont ensuite vérifiées pour leur exactitude absolue par un ordinateur.

Une collaboration s'est formée pour écrire un “plan” lisible par l'homme qui pourrait être utilisé pour cartographier les divers éléments de la preuve en 8 dimensions et déterminer lesquels avaient été formalisés et/ou prouvés, puis prouver et formaliser ces éléments manquants dans Lean. “Nous avions construit le dépôt du projet pendant environ 15 mois lorsque nous avons permis l'accès public en juin 2025,” se souvient Hariharan, maintenant étudiant en première année de doctorat à l'Université Carnegie Mellon. “Puis, fin octobre, nous avons entendu parler de Math, Inc. pour la première fois.”

L'accélération par l'IA

Math, Inc. est une startup développant Gauss, une IA spécifiquement conçue pour formaliser automatiquement des preuves. “C'est un type particulier de modèle de langage appelé agent de raisonnement qui est censé entrelacer à la fois le raisonnement en langage naturel traditionnel et le raisonnement entièrement formalisé,” explique Jesse Han, PDG et cofondateur de Math, Inc. “Ainsi, il est capable de mener des recherches bibliographiques, d'appeler des outils, et d'utiliser un ordinateur pour rédiger du code Lean, prendre des notes, générer des outils de vérification, exécuter le compilateur Lean, etc.”

Math, Inc. a d'abord fait la une des journaux lorsqu'elle a annoncé que Gauss avait complété une formalisation Lean du théorème des nombres premiers forts (PNT) en trois semaines l'été dernier, une tâche sur laquelle le lauréat de la Médaille Fields Terence Tao et Alex Kontorovich avaient travaillé. De même, Math, Inc. a contacté Hariharan et ses collègues pour dire que Gauss avait prouvé plusieurs faits liés à leur projet d'empilement de sphères.

“Ils nous ont dit qu'ils avaient terminé 30 sorrys, ce qui signifiait qu'ils avaient prouvé 30 faits intermédiaires que nous voulions prouver,” explique Hariharan. Une proportion de ces sorrys a été partagée avec l'équipe du projet et fusionnée avec leur propre travail. “L'un d'eux nous a aidés à identifier une faute de frappe dans notre projet, que nous avons ensuite corrigée,” ajoute Hariharan. “C'était donc une collaboration assez fructueuse.”

De 8 à 24 dimensions

Mais ensuite, le silence radio a suivi. Math, Inc. semblait perdre de l'intérêt. Cependant, pendant que Hariharan et ses collègues poursuivaient leur travail passionné, Math, Inc. a...