La preuve dans le code
Recension de The Proof in the Code, de Kevin Hartnett — Quanta, 288 pages, 30 $ américains, parue dans le Wall Street Journal légèrement adaptée pour un public francophone non scientifique. Nos commentaires entre crochets.
Le monde des mathématiques a été ébranlé jusqu'à ses fondements le mois dernier, quand OpenAI a annoncé avoir résolu l'un des problèmes les plus célèbres de la discipline. Le problème de Navier-Stokes [un problème central de la dynamique des fluides : ces équations décrivent l'écoulement de l'eau ou de l'air, et l'on ignore encore si elles admettent toujours des solutions régulières ; c'est l'un des sept « problèmes du millénaire », dotés d'un prix d'un million de dollars chacun], qui porte sur la dynamique complexe des fluides, avait résisté aux assauts des mathématiciens pendant près de deux siècles. Pour en venir à bout, OpenAI a lancé un essaim de 10 000 agents d'intelligence artificielle, qui ont eu besoin de 88 heures pour parvenir au résultat, puis de 17 heures supplémentaires pour le faire confirmer par le programme de vérification informatisée Lean [un « assistant de preuve » : un logiciel qui contrôle, pas à pas, la validité logique de chaque étape d'une démonstration]. En chemin, la société a devancé Tristan Buckmaster, mathématicien à l'Université de New York, et ses collaborateurs, qui étaient sur le point d'aboutir à une solution. L'annonce a été un choc pour nombre de mathématiciens et a suscité un profond questionnement. Mais elle n'aurait peut-être pas surpris Alan Turing.
Turing n'avait que 24 ans en 1936, quand il a imaginé une expérience de pensée simple mais radicale : représentons-nous, proposait-il, une machine composée d'un ruban infini divisé en cases où sont écrits des signes, et d'une « tête » (c'est son terme) capable de lire et d'écrire des signes. La tête lirait le signe contenu dans une case, répondrait en écrivant un autre signe, puis passerait à la case suivante et recommencerait — le tout selon un ensemble de règles fixées à l'avance. La proposition paraissait à la fois triviale et inutile : après tout, la machine ne « fait » rien d'autre que transformer des signes dépourvus de sens en d'autres signes dépourvus de sens. Et pourtant, la « machine de Turing », comme on finirait par l'appeler, a fourni les fondements théoriques de tous les ordinateurs conçus depuis.
Turing n'était pas informaticien, même s'il a inventé la discipline. C'était un mathématicien, et sa machine incarnait le « formalisme » [une école de pensée selon laquelle faire des mathématiques, c'est déplacer des symboles selon des règles convenues, sans se préoccuper de leur « sens »] — une idée qui transformait alors son domaine : loin d'être l'étude de vérités universelles, les mathématiques ne seraient rien d'autre que la manipulation de signes dépourvus de sens selon des règles prédéterminées. Quoi de plus approprié, dès lors, qu'une machine qui fait exactement cela ? Il s'ensuivait que la machine de Turing pouvait produire toutes les mathématiques possibles — et bien mieux qu'un être humain, par nature sujet à l'erreur.
Comme le raconte Kevin Hartnett dans The Proof in the Code (« La preuve dans le code »), dès que les premiers ordinateurs numériques furent disponibles, leurs créateurs cherchèrent à mettre la proposition de Turing à l'épreuve. Dans les années 1950 et 1960, des chercheurs mirent au point des « prouveurs » automatiques de théorèmes (ATP), capables d'examiner de longues formules mathématiques pour déterminer si elles étaient vraies sous certaines conditions. Les ATP se révélèrent puissants et efficaces — du moins pour certains types de problèmes.
Lean fut d'abord un programme conçu pour déceler les bogues des produits de Microsoft. Il a fini par révolutionner les mathématiques.
Il apparut toutefois clairement que la plupart des questions qui intéressent les mathématiciens ne se prêtent pas si facilement à la machine. C'est pourquoi, quitte à transiger sur l'idéal de la démonstration mécanisée, les chercheurs développèrent les assistants interactifs de preuve (ITP) : le mathématicien propose une argumentation formelle, et le programme vérifie si elle est correcte, et à quelles conditions. Grâce à cet outil plus souple, Kenneth Appel et Wolfgang Haken réussirent en 1976 à démontrer le théorème des quatre couleurs [l'affirmation que quatre couleurs suffisent pour colorier n'importe quelle carte de façon que deux régions voisines ne portent jamais la même couleur], qui tenait en échec les mathématiciens depuis plus d'un siècle ; et Thomas Hales fit de même pour un problème plus prestigieux encore : la conjecture de Kepler, vieille de quatre siècles [la question de savoir comment empiler des sphères identiques — des oranges, par exemple — pour qu'elles occupent le moins d'espace possible].
Même ainsi, les ITP restèrent impopulaires auprès des mathématiciens en exercice. Ces derniers découvrirent vite que rendre une argumentation mathématique compréhensible pour un programme informatique exigeait un travail colossal. Il fallait réduire le raisonnement à un enchaînement formel d'étapes à donner le vertige — et en faire autant pour toutes les mathématiques sur lesquelles il reposait. Dans leurs échanges ordinaires, les mathématiciens s'appuient sur un vaste fonds de savoir qu'ils peuvent tenir pour acquis chez leurs collègues. Pour soumettre un raisonnement à un ITP, tout cet arrière-plan doit être saisi, explicitement et formellement, jusqu'aux définitions les plus élémentaires des nombres. Paradoxalement, s'attaquer à un problème mathématique à l'aide de l'ordinateur se révélait souvent bien plus laborieux que le traiter à la méthode traditionnelle.
The Proof in the Code raconte l'histoire de Lean, l'ITP qui a fini par installer la démonstration par ordinateur au cœur des mathématiques contemporaines. Lean est né de l'imagination de Leonardo de Moura, informaticien chez Microsoft Research au début des années 2000. Son objectif initial était modeste : créer un programme capable de repérer les bogues cachés dans les produits Microsoft. Son programme Z3 s'avéra très efficace à cette tâche pour Windows 7, avant sa sortie en 2009, et Lean devait aller plus loin : là où Z3 ne pouvait vérifier que des exécutions particulières d'un programme avec des valeurs particulières, Lean fut conçu pour traquer les bogues dans les programmes pris dans leur ensemble.
De Moura comptait sans doute mettre Lean au service de la rentabilité de Microsoft ; il découvrit pourtant rapidement que les personnes les plus intéressées par le programme étaient les mathématiciens. Chercher les bogues d'un programme informatique, il se trouve, se distingue à peine de la vérification d'une démonstration mathématique formelle — précisément le travail des ITP. M. de Moura se mit donc à travailler de près avec un petit cercle de mathématiciens résolus à faire de l'ordinateur un outil standard de leur discipline.
[L'auteur du livre] Hartnett brille surtout lorsqu'il peint les personnalités et les dynamiques de ce petit cercle. M. de Moura, brillant mais effacé, maintient le projet sur les rails à force d'acharnement. Son plus proche collaborateur, Jeremy Avigad, est un mentor universitaire dans la plus pure tradition, qui rallie ses étudiants à la cause. Mario Carneiro, plus jeune, se heurte parfois à M. de Moura ; il possède une passion inextinguible pour la formalisation des démonstrations. Kevin Buzzard, théoricien des nombres britannique haut en couleur, est convaincu que Lean va débarrasser les mathématiques de leur laisser-aller excessif.
Pour conjurer la besogne de Sisyphe qu'aurait représentée la formalisation, à partir de zéro et à chaque fois, de toutes les mathématiques pertinentes, les enthousiastes de Lean décidèrent de créer Mathlib [une bibliothèque où sont rassemblés des milliers de résultats mathématiques déjà formalisés, les lemmes, afin que les nouvelles démonstrations puissent s'appuyer sur ce socle commun] — une bibliothèque de mathématiques formalisées. Ce fut une entreprise de longue haleine et sans terme défini, qui provoqua des frictions au sein de l'équipe. En particulier, M. de Moura, absorbé par l'amélioration des capacités fondamentales de Lean, passait de longues heures chaque jour à corriger les entrées de Mathlib soumises par d'autres contributeurs, qui lui paraissaient exigeants et peu respectueux. Mais à mesure que la bibliothèque grossissait et que sa réputation se répandait, toujours plus de mathématiciens furent attirés par la contribution, et rejoignirent le cercle Lean.
Une percée survint fin 2020. Peter Scholze, lauréat de la médaille Fields (surnommée « le Nobel des mathématiques »), demanda de l'aide à M. Buzzard : Lean pourrait-il vérifier sa démonstration la plus récente et la plus ardue, dans un domaine appelé « tenseurs liquides » [un domaine sans rapport avec les liquides ordinaires — le nom désigne certains espaces de fonctions particuliers] ? Comme cette démonstration reposait sur une montagne de résultats antérieurs, la faire passer par Lean exigeait de formaliser tout ce savoir mathématique et de l'inscrire dans Mathlib. Le projet mobilisa 28 mathématiciens et 18 mois de travail ; mais en juillet 2022, M. Scholze annonçait que Lean avait vérifié sa démonstration. Un an plus tard, Terence Tao, de l'Université de Californie à Los Angeles — autre médaillé Fields, et peut-être le mathématicien le plus influent du monde — réunit un groupe encore plus vaste pour utiliser Lean à vérifier sa démonstration de la conjecture polynomiale de Freiman-Ruzsa [une conjecture de combinatoire additive, domaine qui étudie notamment les propriétés des ensembles de nombres sous l'addition]. Il n'était plus possible d'en douter : Lean était devenu un pilier des mathématiques de pointe.
Mais alors même que Lean faisait ses preuves, une autre révolution se jouait hors des amphithéâtres. D'abord OpenAI, puis de nombreuses autres sociétés, se mirent à offrir de grands modèles de langage (LLM) capables d'écrire de la prose, de traduire la parole, de produire des vidéos à la demande, et bien davantage. Entraînés sur des masses sidérantes de sources produites par des humains, ces LLM recourent à des algorithmes statistiques pour produire des résultats quasi impossibles à distinguer de créations humaines.
Les LLM fournissaient des résultats déplorables en mathématiques — jusqu'à ce que des humains les branchent sur un programme nommé Lean. Une boucle de rétroaction a permis d'aboutir à des démonstrations correctes.
Au départ, les LLM étaient en effet pitoyables en mathématiques. Quand on leur demandait de générer une démonstration, ils produisaient un texte [de manière probabiliste en devinant le mot suivant le plus probable] qui en avait l'apparence, mais logiquement incohérent. Puis Thomas Hubert, chez DeepMind (Google), trouva le moyen d'améliorer leurs performances : au lieu de s'en tenir à une mauvaise « preuve », les LLM soumettraient leur premier jet à Lean, qui leur renverrait son opinion. Le LLM s'appuierait sur ce retour pour produire une version meilleure, qu'il soumettrait de nouveau à Lean. Après de nombreuses itérations, le système d'IA pouvait produire une démonstration correcte. Ce cycle, démultiplié par l'usage d'agents d'IA autonomes, s'est révélé déterminant dans le résultat d'OpenAI sur Navier-Stokes.
Sommes-nous enfin en présence d'une véritable machine de Turing, capable de produire des mathématiques avancées sans intervention humaine ? On peut sérieusement le soutenir. Et pourtant, à la lecture de The Proof in the Code, qui conduit le lecteur jusqu'au seuil des percées actuelles, l'auteur de l'article a été frappé autant par les limites des mathématiques produites par les machines que par leur puissance. Lean peut vérifier n'importe quel enchaînement de déductions, mais il repose toujours sur Mathlib — un corpus mathématique créé par des humains, jugé important et porteur de sens par des humains.
De même, la démonstration de Navier-Stokes par OpenAI fut, sans l'ombre d'un doute, un exercice fantastiquement complexe de manipulation de signes. Mais ce sont des humains qui ont jugé important de dépenser des millions de dollars en agents d'IA pour se livrer à cet exercice particulier de manipulation de signes. Il faut donc se demander : une méthode de démonstration qui se passe de l'intuition humaine et doit être admise sur parole peut-elle être tenue pour des mathématiques ? Dans une lettre récente, plus de 25 médaillés Fields (dont MM. Scholze et Tao) ont répondu : « non ». La démonstration d'OpenAI est presque certainement correcte. Mais un résultat qui ne fait rien pour faire progresser la compréhension humaine, soutiennent-ils, peut difficilement être appelé mathématiques.
La discipline est à un tournant. L'adoption généralisée de Lean et les percées des LLM obligent les mathématiciens, pour la première fois depuis plus d'un siècle, à revisiter les fondements de leur domaine. Qu'est-ce qui mérite d'être appelé mathématiques ? Qu'est-ce qu'une démonstration ? Et à qui, de l'humain ou de la machine, revient le mérite ? The Proof in the Code, de Kevin Hartnett, est un récit vivant et profondément humain du chemin qui nous a menés jusqu'ici.
Voir aussi
IA — L'apocalypse de l'emploi est reportée
Quand les livres deviennent innombrables, à quoi servent encore les éditeurs ?
Les IA corrompent insidieusement les documents qu’on leur soumet
L’IA fragilise les indices superficiels de sérieux scientifique
Pourquoi, malgré les prédictions, l'IA n'a pas remplacé les radiologues (pour l'instant ?)
L'IA est-elle déjà en train de priver les diplômés d'emploi ?
Apocalypse professionnelle ? Pas pour l'instant : l'IA crée de tout nouveaux métiers










.webp)

