La preuve dans le code
Kévin Hartnett
Livres Quanta, 30 $
En 2024, l’Olympiade internationale de mathématiques a accueilli un participant inhabituel. Google Deepmind avait mis AlphaProof, un programme d'IA nouvellement formé, sur les questions du concours de cette année-là, bien qu'en tant que participant non officiel. Dans le cadre du concours, les meilleurs étudiants en mathématiques du monde entier résolvent six problèmes de mathématiques avancés sur deux jours. AlphaProof a fait la une des journaux et a atteint le seuil de la médaille d'argent en marquant 28 points sur 42.
AlphaProof est un solveur de théorèmes mathématiques, un système permettant de prouver des énoncés mathématiques. Il y a à peine quatre ans, entraîner des systèmes d’IA à automatiser le raisonnement mathématique représentait un défi de taille. Mais Google Deepmind et d’autres groupes espéraient que leurs efforts permettraient de doter les systèmes d’IA de compétences de raisonnement plus larges qui pourraient un jour être appliquées à des problèmes du monde réel, en utilisant la logique pour potentiellement libérer les outils d’IA des hallucinations, des instances d’informations inventées.
Beaucoup de ces programmes doivent leur succès au programme d’assistant de preuve Lean. Leo de Moura a lancé Lean comme outil de vérification du code logiciel en 2013 alors qu'il était ingénieur logiciel chez Microsoft Research. Mais aujourd’hui, les mathématiciens et les chercheurs en IA sont les plus grands partisans du Lean. Dans son nouveau livre Le Preuve dans le Codele journaliste Kevin Hartnett retrace cette évolution.
Hartnett raconte la persistance de de Moura à développer des logiciels qui n'avaient aucun avantage commercial immédiat et la détermination obstinée d'un petit groupe de mathématiciens qui ont persuadé leur domaine d'adopter le programme. Tout au long du livre, Hartnett présente une multitude de personnages du monde entier qui ont vu dans Lean une nouvelle façon d'évaluer les vérités mathématiques et ont joué un rôle, grand et petit, pour rendre Lean plus convivial. Ensemble, cela constitue une histoire de collaboration inspirante.
Dans les premiers chapitres, Hartnett parsème d'explications sur les similitudes entre les mathématiques et le codage, démontrant comment l'utilisation du Lean pourrait si naturellement être transplantée dans la recherche mathématique. « Les deux sont écrits dans une syntaxe exacte sous la forme d'une série d'étapes logiques, chacune menant à la suivante », écrit Hartnett. « Une lacune dans la logique d'une preuve est comme un bug dans le code d'un logiciel. » Un programme s'exécute lorsque le code a la bonne logique. Un nouveau théorème mathématique est le résultat d’une preuve correctement écrite.
Presque immédiatement après le lancement de Lean, Jeremy Avigad de l'Université Carnegie Mellon a commencé à le mettre en place pour rédiger des épreuves de mathématiques. Le Lean et d'autres programmes d'assistance à la preuve, également connus sous le nom de prouveurs de théorèmes interactifs, peuvent vérifier de nouvelles preuves mathématiques écrites par des humains, qui s'étendent parfois sur des centaines de pages et peuvent prendre des mois à examiner. Les programmes ne peuvent pas proposer de nouvelles preuves, mais en contribuant à garantir que les preuves sont exemptes d'erreurs, ils peuvent permettre aux mathématiciens d'établir plus rapidement de nouveaux faits mathématiques pour les utiliser dans des preuves plus récentes. Pourtant, les assistants de preuve étaient des logiciels encombrants qui nécessitaient d’écrire les mathématiques d’une manière totalement différente.
Pour travailler avec des assistants de preuve, les mathématiciens devaient traduire des problèmes du langage simple en code et créer des bibliothèques de définitions codées et de théorèmes de concepts mathématiques de base. Par exemple, lorsque Kevin Buzzard, professeur de mathématiques à l'Imperial College de Londres, rédigeait des séries de problèmes pour apprendre à ses étudiants de premier cycle à travailler avec Lean, il s'est rapidement heurté à un obstacle inattendu. « Lean lui a demandé de prouver que 2 n'est pas égal à 1 », écrit Harnett. « C'est une affirmation si clairement vraie que les êtres humains, dans une conversation normale, ne perdraient pas un instant à la justifier. » Mais Lean lui a demandé de prouver l’inégalité avant de l’utiliser.
Pendant longtemps, il n’y avait tout simplement pas assez de mathématiques dans les bibliothèques Lean pour qu’elles soient utiles aux mathématiciens. Et il serait impossible de coder davantage de mathématiques sans que davantage de mathématiciens utilisent le programme. Hartnett partage ce qu'il a fallu à certains mathématiciens pour populariser le Lean. Par exemple, en 2018, Buzzard et d’autres ont entrepris de traduire les espaces perfectoïdes en Lean. Le codage de cette nouvelle innovation étincelante en géométrie arithmétique leur a demandé des mois de travail et plusieurs milliers de lignes de code. Et ces efforts ont fonctionné. En 2025, « des dizaines de milliers d’utilisateurs du monde universitaire et technologique lançaient des projets de plus en plus ambitieux en plus du Lean », écrit Hartnett. Cela incluait des chercheurs en IA, qui avaient trouvé dans Lean une vaste bibliothèque de mathématiques avancées nécessaires à la formation de modèles d'IA de résolution mathématique tels qu'AlphaProof.
De Moura et les mathématiciens voulaient construire une machine de vérité, « un programme informatique capable de fournir une garantie complète à 100 % qu'une chaîne logique est correcte », écrit Hartnett. Alors que pour de Moura, la vérité qu'il recherchait était de savoir avec certitude que le code des programmes informatiques, comme Microsoft Word, était correct et exempt de bogues, pour les mathématiciens, une machine de vérité pourrait rendre les découvertes de preuves mathématiques plus rigoureuses, organisées et exactes.
Acheter La preuve dans le code de Bookshop.org. Actualités scientifiques est affilié à Bookshop.org et gagnera une commission sur les achats effectués à partir des liens contenus dans cet article.
