Maths 2.0 : quand l'IA publie 722 preuves en une nuit

Terence Tao, souvent décrit comme le porte-voix officieux des mathématiques, vient de répondre au déluge : des centaines de percées mathématiques produites par l'intelligence artificielle et publiées par OpenAI en quelques jours. L'animateur, Samuel Allen Alexander, relit le mémo Maths 2.0 de Tao ligne par ligne pour le discuter. La question est simple et vertigineuse : quand les machines démontrent des théorèmes, à quoi servent encore les mathématiques ?

Dans le récit que Tao fait de l'ordre classique, les Maths 1.0, la preuve d'une conjecture ancienne déclenche une vaste réaction en chaîne : les auteurs sont invités à donner des exposés, ils rencontrent les spécialistes, des ateliers s'organisent, de nouvelles collaborations naissent, des problèmes dérivés circulent, et les preuves se simplifient jusqu'aux notes de cours. Cette digestion transforme un résultat en bien commun du domaine.

La promesse des Maths 1.0 : la preuve digérée

L'objection de Tao est tranchante : un problème résolu ne peut redevenir non résolu, et la simple connaissance d'une solution contamine la recherche d'autres voies. Selon lui, des équipes assistées par l'IA moissonnent désormais les problèmes ouverts à l'échelle industrielle, une logique de moisson des preuves qui épuise le sol même qui rendait les domaines fertiles. Là où la prime au premier arrivé s'efface, le mécanisme qui récompensait la pensée profonde s'affaiblit aussi.

Le débat s'est enflammé début septembre avec l'annonce d'OpenAI sur la régularité de Navier-Stokes. Dans un entretien accordé à IBM, Tao a jugé l'événement très préoccupant : quand des nœuds vieux de quatre-vingt-dix ans comme Navier-Stokes se dénouent avant que méthodes et intuitions intermédiaires soient distillées, les sous-produits du chemin se perdent. L'IA aurait ainsi dépassé les étalons pour collectionner les problèmes ouverts un par un.

Début octobre, le tableau s'est élargi : 722 articles issus d'un modèle frontière non publié, 372 familles de résultats dans une vingtaine de sous-domaines. Selon NewScientist, Francis Johnson, qui a consacré vingt-cinq ans au problème D(2) de Wall et écrit deux livres sur le sujet, a accueilli le résultat avec stupéfaction. SiliconAngle signale un morceau quasi-Riemann touchant à l'hypothèse de Riemann, vieille de cent cinquante ans, ainsi que plus de quatre-vingts travaux sur la multiplication matricielle et l'informatique théorique.

Le déluge d'octobre : 722 articles en une nuit

Une analyse d'Implicator relève que 42 pour cent seulement des résultats vedettes portaient un certificat Lean vérifié par machine ; le modèle non publié ne peut être réexécuté de l'extérieur et aucun énoncé n'a été partagé. Le lendemain, trois manuscrits étaient retirés pour une erreur de signe. L'épisode montre pourquoi la vérification Lean doit séparer les manchettes certifiées des affirmations brutes, réserve que l'entreprise admet elle-même.

Alexander, l'animateur, juge ce tableau peint depuis la fenêtre de l'élite. Il raconte avoir publié l'an dernier dans une revue de premier plan en biologie mathématique sans recevoir aucune invitation à exposer. Les chercheurs ordinaires, dit-il, ne voient jamais ce faste ; Wiles gardant son travail sur Fermat secret pendant des années prouve que la rétention d'information précède l'IA. Et avec des millions de preuves de Pythagore, personne n'est empêché d'en chercher une de plus.

Le front Hacker News : combiner ou créer

Sur Hacker News, Love Parade résume le motif avec netteté : les modèles excellent à combiner d'immenses savoirs mais peinent à prendre du recul pour proposer une abstraction élégante. Fotron défend la thèse de la boucle de rétroaction étroite : quand le résultat se vérifie aisément, les modèles brillent, ce qui explique le succès des assistants de preuve couplés à l'IA. Alexander répond par son vécu : des spectateurs ont résolu par l'IA des problèmes ouverts de ses propres articles, avec un vrai souffle original.

Fubble rappelle que les laboratoires ont proclamé leur supériorité au go et aux échecs avant de se retirer : les mathématiques seront-elles abandonnées une fois les jalons épuisés ? Ant-Man parie que les hallucinations s'estomperont, que les sorties se simplifieront et que l'humain quittera la boucle. L'animateur, lui, exulte : voici l' âge d'or le plus exaltant depuis Euclide, et les seuls à passer un mauvais moment siègent dans les chaires d'élite.

La formule de Bner pourrait résumer le débat : l'avenir des mathématiques n'est pas de résoudre mais de raconter ce qui fut résolu et pourquoi cela compte. La remarque psychologique de Thurston appartient à ce tableau : les mathématiques sont la discipline des idées qui résistent au passage d'un esprit à l'autre. Comme le montre le dossier de QuantaMagazine, les vérificateurs assistés par LLM permettent de découper un problème en morceaux, de les résoudre un par un et de réassembler le tout en confiance.

Beauté, financement et philosophie

L'éloge russellien de 1902, beauté froide et austère, et le critère de Hardy, nulle place durable pour des mathématiques laides, occupent un long passage de la vidéo. L'animateur les retourne : si les mathématiques pures sont un art et une science sociale, le contribuable financera la recherche avec moins d'entrain. L'épopée des nombres premiers vers la cryptographie relèverait du biais du survivant : une poignée de résultats utiles masque des millions d'oubliés. Le critère de beauté peut durer, mais pas servir de dossier de financement.

Un billet invité sur le carnet WordPress de Tao resserre le cadre avec la maxime de Rav : les théorèmes sont les gros titres, les preuves sont l'histoire intérieure. L'annonce Navier-Stokes du 8 septembre, y lit-on, vint d'environ dix mille agents explorant en parallèle, puis fut formalisée en Lean : exactitude soutenue par la machine, intuition pas encore digérée. Gowers ajoute la même note : des rédactions machine médiocres ne sont peut-être qu'un tracas passager. Sans l' histoire intérieure , le titre reste mince.

Reste le devoir des Maths 2.0 : convertir le déluge de solutions en compréhension digérée, remettre l'exposé et la construction communautaire au centre. Dans une académie où la prime au premier s'érode et où les montagnes d'articles enflent, le choc de l'IA ouvre aussi une porte à la réforme. La parabole de la fabrique de crayons de l'animateur convient : face à la surabondance, la réponse n'est pas plus de crayons. Lire davantage, trier, raconter ; distiller le sens, pas les jetons.