Le lundi 19 octobre, la revue de vulgarisation Quanta a publié le verdict des spécialistes qui ont examiné une preuve mathématique réalisée par une intelligence artificielle (IA) d'OpenAI : dans l'ensemble, ils s'accordent à dire que le résultat est correct. L'un d'eux, Maksym Radziwiłł, de l'Université de New York, a souligné que les implications de cette avancée partielle sont “étonnantes”, exprimant l'idée que, dans un certain sens, la grande majorité des conséquences de l'hypothèse complète découlent de cette démonstration.
S'ils disent que c'est bon, pourquoi ne la donne-t-on pas encore pour terminée ?
La réponse n'est pas qu'il n'y ait pas de consensus. Et la comprendre sert à juger si cette preuve est le plus grand exploit de l'IA, et tous ces titres que nous voyons sur l'IA découvrant des choses.
Cette démonstration a été rendue publique le mardi 6 octobre, lorsque OpenAI a publié un lot de 722 travaux de mathématiques réalisés, selon l'entreprise, par une IA interne qui n'est pas encore sortie au public : une qui ne se trouve pas encore dans ChatGPT.
Parmi ces travaux se trouvait celui qui aborde l'hypothèse de Riemann, une question sur les nombres premiers ouverte depuis plus de 160 ans. Bien qu'elle ne la résolve pas, elle présente la preuve d'une version plus faible, l'hypothèse quasi-Riemann.
Pour comprendre le verdict, il faut distinguer deux choses qui en mathématiques vont souvent ensemble : qu'une preuve soit correcte et que d'autres puissent la suivre. Aujourd'hui, le premier point peut être contrôlé, en partie, par un programme ; le second relève des personnes.
Que dit l'hypothèse de Riemann, vue comme une route
Un nombre premier est un entier supérieur à un qui n'est divisible que par lui-même et par l'unité : 2, 3, 5, 7. Ils apparaissent de manière éparse, mais il existe une formule qui estime bien combien il y en a jusqu'à n'importe quel nombre (et ce point est clé : c'est une estimation). La grande question est de savoir de combien cette estimation se trompe : sa marge d'erreur, comme dans un sondage.
En 1859, Bernhard Riemann a montré que la manière dont les nombres premiers se répartissent dépend, en un certain sens, des zéros d'une fonction. Une fonction est une règle qui transforme un nombre en un autre, et ses zéros sont les nombres qu'elle transforme en zéro. Chaque zéro a deux coordonnées, comme un lieu sur une carte, et Riemann a prouvé que ceux qui importent tombent dans une bande.
Imaginez cette bande comme une route vue de dessus, et chaque zéro comme une voiture. Plus une voiture se rapproche d'un bord, plus l'estimation des nombres premiers peut être erronée. Riemann a soupçonné que tous vont sur la ligne du milieu, où l'erreur est minimale. C'est l'hypothèse de Riemann : hypothèse, car elle reste à démontrer.
À ce jour, en utilisant la force brute avec des ordinateurs, on a vérifié que les 12 billions premiers zéros se trouvent sur la ligne du milieu. Mais il y en a une infinité, et une preuve doit valoir pour tous.
Que l'IA a prouvé et pourquoi on l'appelle quasi-Riemann
En 1896, il fut prouvé qu'aucune voiture ne franchit la ligne de la rive, et ainsi l'estimation des cousins devint un théorème : quelque chose démontré, qui peut être utilisé sans avoir à le prouver à nouveau. Mais ne pas franchir la ligne n'est pas la même chose que ne pas être collé à celle-ci.
Ce qu’il dit avoir testé avec l’IA est plus fort : si vous divisez la route en 8 voies égales, aucune voiture ne circule sur les deux voies extérieures. La bande vide ne se rétrécit plus : elle a une largeur fixe.
Cela suffit pour tester l'hypothèse quasi-riemannienne. Quasi, de presque : cela ne signifie pas que tout le monde va par le milieu, mais qu'il y a des rives vides d'une largeur fixe.
La bande des zéros vue comme une autoroute : si l'hypothèse est confirmée, aucun véhicule ne circule sur les deux voies extérieures. Que tous empruntent la ligne médiane, comme le soupçonnait Riemann, reste à démontrer.
Cela importe car plus les rives vides sont larges, plus la marge d'erreur est réduite lors du comptage des nombres premiers. Selon Radziwiłł, des dizaines de résultats dépendant de la quasi-conjecture de Riemann seraient démontrés d'un coup si la preuve était confirmée.
Comment vérifier une rédaction générée par une IA
La première version compte 199 pages et correspond à celle des 8 voies. Son résultat principal repose sur Lean, un programme assistant de démonstration de théorèmes qui utilise un langage de programmation fonctionnel permettant d'écrire et de vérifier des démonstrations mathématiques de manière rigoureuse et ligne par ligne, éliminant ainsi la possibilité d'erreurs humaines dans les étapes de la démonstration. Il fonctionne comme un GPS : il garantit que vous êtes arrivé à l'adresse indiquée ; si celle-ci était incorrecte, vous arrivez parfaitement au mauvais endroit.
La deuxième version, terminée quelques jours plus tard et publiée dans le même lot, compte 49 pages et des bords vides plus étroits : ceux de 12 voies, également à largeur fixe.
Les spécialistes ont mis de côté la première version longue pour se concentrer sur la seconde de 49 pages, et Radziwiłł a donné sa raison, très simple : elle est plus courte. La longue a passé le vérificateur et la courte est en cours de révision par les personnes concernées : aucune n'a encore subi les deux contrôles.
Les deux versions du test : le résultat principal de celui de 199 pages a passé par un programme vérificateur ; celle de 49 pages, plus courte et légèrement moins robuste, est celle qu'étudient les spécialistes.Le reste du lot montre pourquoi les deux sont nécessaires. Le mercredi 7 octobre, OpenAI a retiré trois travaux en raison d'une erreur de signe et en a corrigé 14, selon sa page. Il y informe également que près de quatre sur dix ont leur résultat principal vérifié avec Lean ; le reste, non.
Mais le directeur de la bibliothèque de preuves vérifiées de Lean a averti que certaines de ces vérifications semblent prouver quelque chose de plus faible que ce qui est annoncé. C'est comme un GPS qui arrive à une adresse similaire, mais pas à celle annoncée.
Comment comprendre une preuve : de 199 pages à une demi-page
L'IA a d'abord fourni 199 pages, puis une version plus faible de 49 pages. Bien que mal rédigée, les spécialistes la comprennent, et cela se voit à sa réduction : d'autres mathématiciens ont écrit leurs propres versions, de 7 à 13 pages, qui circulent en privé. Et Radziwiłł peut déjà la résumer en une demi-page.
Des 199 pages fournies par l'IA à la demi-page avec laquelle un spécialiste la résume déjà ; entre les deux, les 49 pages de l'autre version de l'IA, plus faible, et celles de 7 à 13 pages écrites par d'autres mathématiciens.
Cette demi-page n'est pas la preuve entière, mais son squelette : la différence entre lire près de 200 pages et la compter sur un coin de nappe. Pour l'instant, cette compression est réalisée par des humains.
Ce sujet suscite un tel intérêt que Peter Sarnak, spécialiste de la théorie des nombres à l'Université de Princeton, a décidé de consacrer le cours de ce semestre à son étude. Mais il ne la considérera pas comme un Théorème, avec une majuscule, tant que les humains n'auront pas examiné et compris tous les détails. C'est pourquoi elle n'est pas encore considérée comme terminée : en mathématiques, une preuve n'est pas terminée quand quelqu'un l'écrit, mais quand d'autres peuvent la suivre.
Alexander Dunn, de l'Institut de technologie de Géorgie, l'a décrite comme « une synthèse surprenante d'idées bien connues », et selon Quanta, une pièce maîtresse est une formule qu'il a démontrée avec Radziwiłł en 2021. Les spécialistes pensaient qu'il faudrait une autre branche de la théorie des nombres. L'IA a travaillé comme si les outils habituels suffisaient : « une croyance assez audacieuse », selon Radziwiłł. Si la preuve tient, il a eu raison.
Cela ne signifie pas que la preuve que toutes les voitures roulent sur la voie de droite est proche. Will Sawin, également de Princeton, pense que l'hypothèse complète restera « aussi éloignée qu'avant », bien qu'il n'en soit pas sûr.
Que penser de l'étiquette de plus grande réussite de l'IA
Sert-elle à quelque chose en dehors des mathématiques ? Pour l'instant, si la preuve est confirmée, certains calculs que les ordinateurs effectuent en testant des nombres au hasard auraient une recette sans aléa et donc un temps maximal garanti, bien qu'ils se résolvaient déjà rapidement avec de l'aléatoire. Ce que la preuve débloque, ce sont d'autres théorèmes.
Est-ce donc la plus grande réussite de l'IA en mathématiques ? Pour Jared Duker Lichtman, de l'Université de Stanford, oui : il l'a appelée « la réalisation la plus significative de l'IA en mathématiques jusqu'à présent, et de loin ». Il convient de savoir que Lichtman a collaboré avec Math, Inc., une entreprise d'IA pour les mathématiques. Et il convient de lire les petites lignes. Il dit « de l'IA » et « jusqu'à présent » : il compare l'IA à elle-même, pas à toute l'histoire des mathématiques.
Ma lecture, discutable, est que Lichtman a de bonnes raisons, mais cette étiquette est encore écrite au crayon : cela vaut si la preuve tient debout, et c’est aux personnes qui la lisent de décider. Le fond du problème est autre chose. L’IA produit déjà des preuves plus rapidement que les mathématiciens ne peuvent les lire : le goulot d’étranglement n’est plus de trouver la preuve ; il est désormais de la comprendre.
Ceux et celles qui travaillons avec ces systèmes connaissons la petite version de ce décalage : produire est devenu bon marché ; réviser, non.
La prochaine fois que vous lisez qu’une IA a démontré quelque chose, posez-vous trois questions. Les experts indépendants le confirment-ils, et pas seulement l’entreprise ? La révision a-t-elle été faite par des humains, et pas seulement par un programme ? Un spécialiste extérieur a-t-il déjà pu la résumer en quelques pages ?
Avec la preuve des rives vides, la première réponse est oui, la seconde est mitigée et la troisième tient déjà en une demi-page.