La pharmacologie connaît de longue date l’écart entre savoir qu’un remède agit et savoir pourquoi. Commercialisée par Bayer en 1899, l’aspirine a soulagé des générations de patients avant que le Britannique John Vane n’établisse, en 1971, qu’elle bloque la synthèse des prostaglandines, découverte couronnée par le prix Nobel de médecine en 1982.
Les mathématiques tenaient les deux ensemble : une démonstration certifie un énoncé et, du même geste, fait voir pourquoi il est vrai. Le lien se défait quand des machines livrent des dizaines de pages qu’un logiciel valide pas à pas avant qu’un spécialiste les ait lues. Le 26 octobre, OpenAI a revendiqué pour ses modèles internes trois résultats de ce genre ; le lendemain, Anthropic revendiquait à son tour l’un des trois.
Dans ces annonces, la réponse précède l’explication au lieu de l’accompagner. Reste à établir ce que chaque résultat affirme, ce que garantit la vérification formelle et ce qu’elle laisse au lecteur, puis à qui reviennent, quand une partie des pièces demeure fermée, le travail de comprendre et le crédit qui s’y attache.
Trois résultats, trois régimes de publication
OpenAI range ses trois résultats en analyse harmonique, en théorie de la complexité et en théorie quantique des champs, sur des questions en suspens depuis des décennies, et présente les manuscrits comme des « données de recherche brutes ». Ils viennent de modèles internes, comme celui qui avait réfuté la conjecture d’Erdős sur les distances unités, dont OpenAI a détaillé l’évasion du bac à sable le 20 juillet.
La réfutation de l’hypothèse du temps exponentiel aurait été trouvée le 16 octobre et formalisée dans l’assistant de preuve Lean le 17, la conjecture sur les ondes les 18 et 19 octobre ; les preuves de physique remontent aux 9 et 18 septembre. Les mathématiques sont livrées brutes, sans lecteurs désignés, l’informatique confiée à un groupe extérieur chargé de l’expliquer, matériaux publics, la physique à un groupe maître de la publication, dont rien n’est sorti. OpenAI dit ignorer laquelle de ces voies sera la plus utile.
Une onde qui se focalise, une aiguille qui tourne
La conjecture de Christopher Sogge
Proposée en 1991 par Christopher Sogge, la conjecture du lissage local affirme qu’une onde ne reste pas longtemps focalisée : issue d’une mince coquille sphérique, elle peut devenir bien plus intense à l’instant où ses rayons convergent, mais, moyennée sur un intervalle de temps, elle se tient nettement plus bas qu’à son pire instant. Selon OpenAI, la démontrer règle deux autres conjectures majeures, celle de restriction de Stein et celle de Kakeya, née en 1917 d’une question de Sōichi Kakeya : comment faire pivoter une aiguille dans toutes les directions en balayant le moins de place possible.
Kakeya avant l’annonce
Le lissage local n’était établi qu’en deux dimensions d’espace, par Larry Guth, Hong Wang et Ruixiang Zhang en 2019. La conjecture de Kakeya, qui veut qu’un ensemble contenant un segment dans chaque direction ait la dimension pleine, ne l’était qu’en dimension 2 et, depuis février 2025, en dimension 3, grâce à Hong Wang et Joshua Zahl ; ce travail a notamment valu en juillet la médaille Fields à Hong Wang, professeure permanente à l’IHES de Bures-sur-Yvette. Le 6 octobre, le dépôt d’OpenAI revendiquait déjà la dimension 3 du lissage local et la dimension 4 de Kakeya.
Le manuscrit d’OpenAI, 59 pages datées du 25 octobre, revendique toutes les dimensions et en déduit aussi la conjecture de Bochner-Riesz et les conjectures maximales de Kakeya et de Nikodym. Là où l’on découpait l’onde en fins secteurs angulaires, sa preuve construit un courant conservé pour une superposition d’ondes. L’enjeu, pour l’analyse harmonique, serait de premier ordre.
L’hypothèse du temps exponentiel
Une conjecture plus exigeante que P différent de NP
Le problème 3-SAT demande s’il existe une façon d’attribuer vrai ou faux à n variables qui satisfasse des contraintes portant chacune sur trois d’entre elles : il faut repérer, dans une foule de combinaisons dont l’essai exhaustif coûte 2 puissance n, celle qui convient. Formulée à la fin des années 1990 par Russell Impagliazzo et Ramamohan Paturi, avec Francis Zane, l’hypothèse du temps exponentiel, ou ETH, postule que le temps de calcul croît forcément de façon exponentielle avec le nombre de variables. Plus forte que P différent de NP, elle étaye des centaines de résultats, plus de 800 articles selon un recensement cité par Anthropic.
Un algorithme qui compte toutes les solutions
Le manuscrit d’OpenAI, « The Exponential Time Hypothesis is False », 67 pages datées du 17 octobre et révisées le 25, décrit un algorithme déterministe qui compte exactement les solutions d’une formule à clauses de largeur fixe, en mémoire polynomiale et en temps sous-exponentiel : l’exposant croît à peu près comme n divisé par la racine carrée de son logarithme. La voie principale est algébrique, par le comptage des zéros communs de systèmes polynomiaux creux ; seule l’annexe qui donne la meilleure borne contracte des réseaux de tenseurs. Le texte dit réfuter aussi les variantes renforcées SETH, Gap-ETH et NSETH.
Ce qui tombe, ce qui tient
Confirmée, la réfutation ébranlerait des décennies de travaux sans trancher P contre NP, l’algorithme restant plus lent que tout polynôme, ni accélérer les machines d’aujourd’hui. Un tel temps ne se transmet pas par les réductions usuelles, qui font gonfler le nombre de variables : rien de neuf pour la somme de sous-ensembles ou le voyageur de commerce. Les théorèmes conditionnels de la complexité dite fine restent vrais comme implications, privés de leur prémisse, et des bornes comme celle de la plus longue sous-suite commune survivent, car elles découlent aussi de la conjecture des vecteurs orthogonaux, toujours debout.
Le gain est galactique : d’après Anthropic, sa borne ne bat la force brute, pour des formules à cinq clauses par variable, qu’au-delà d’un nombre de variables à plus de dix mille chiffres, quand la force brute est déjà impraticable à cent variables. Le résultat, conclut le texte, ne dit rien de la résolution pratique des formules.
Anthropic, le lendemain, par une autre voie
Le 27 octobre, Anthropic a mis en ligne sur le serveur de prépublications Hexagon « A 2^o(n) Time Algorithm for 3-SAT », 49 pages signées « Claude, Anthropic », avec une formalisation en Lean 4 versée sur GitHub. L’algorithme central aurait été trouvé le 16 octobre par un modèle de recherche interne, en 14 millions de jetons de sortie et sans intervention humaine, des chercheurs ayant ensuite retravaillé la présentation avec lui. Le texte précise que, « indépendamment et simultanément », un modèle interne d’OpenAI dit avoir prouvé un résultat similaire.
Les chemins diffèrent : là où le corps du texte d’OpenAI passe par l’algèbre des polynômes, Anthropic contracte d’emblée des réseaux de tenseurs, autour d’une identité des huit carrés liée aux octonions. Datée du même jour par deux rivaux aux routes distinctes, la réfutation gagne en plausibilité. Levent Alpöge, chercheur d’Anthropic, opposé à OpenAI avec Tristan Buckmaster le 8 septembre sur les équations de Navier-Stokes, l’a relayée. Le 28 octobre, Lance Fortnow, de l’Illinois Tech, admet n’avoir pas vérifié la preuve mais tient désormais l’ETH pour « fichue », et signale des versions simplifiées de Ryan O’Donnell et Shiva Kintali.
Ce que Lean certifie, ce qu’il laisse au lecteur
Une borne plus faible dans le fichier que dans le papier
Lean vérifie que chaque pas découle des axiomes, non que l’énoncé formalisé traduise le problème étudié. Les dix résultats attribués début août à une version interne d’Astra arrivaient déjà avec des certificats en Lean 4 ; la fiche 378 du dépôt openai/math montre cette fois l’écart sur pièces. Lean y démontre une borne un peu plus faible que celle du manuscrit, le facteur log log n figurant au carré dans l’exposant, pour un modèle de machine et un encodage « canonique » des formules définis par OpenAI. Le temps sous-exponentiel est couvert, le chiffre exact du papier ne l’est pas.
Une traduction que personne n’a encore relue
Anthropic écrit la limite noir sur blanc : « Lean vérifie les preuves, mais aucune machine ne vérifie que ce fichier dit ce que dit le papier. » Sa chaîne est soignée, avec l’outil Comparator, qui confronte les énoncés à une référence, et un second noyau indépendant, nanoda ; mais la formalisation, écrite par des modèles, n’a été relue que par d’autres instances des mêmes modèles, et nul n’est connu pour l’avoir vérifiée. Le filtre formel déplace la confiance vers un court fichier de définitions qu’un spécialiste doit juger fidèle. Le non-formalisé a ses risques : le 7 octobre, OpenAI a retiré trois manuscrits liés à la conjecture de Hodge, ruinés par une erreur de signe.
Yang-Mills, l’existence sans le trou de masse
En physique, OpenAI dit tenir une preuve rigoureuse que des théories quantiques des champs en interaction existent en quatre dimensions, dont la théorie de Yang-Mills pure, la chromodynamique quantique et une « complétion unifiée » du modèle standard. Le problème du millénaire du Clay Mathematics Institute, énoncé en 2000 par Arthur Jaffe et Edward Witten, exige qu’une théorie de Yang-Mills quantique non triviale existe pour tout groupe de jauge compact simple et qu’elle présente un « trou de masse », un écart d’énergie strictement positif au-dessus du vide. OpenAI ne revendique que l’existence, soit un volet du problème.
Formalisée selon OpenAI le 16 octobre pour Yang-Mills, la preuve n’est pas publique. Sa lecture revient à un groupe que conduit David Gross, lauréat du Nobel de physique en 2004, avec Michael Douglas, Arthur Jaffe, Igor Klebanov et Nikita Nekrasov, qui rédigera lui-même un texte intelligible plutôt que de publier les artefacts du modèle. Hors du groupe, aucune vérification indépendante n’est possible. Dès le 26 octobre, l’AGMAI, groupe consultatif sur les mathématiques et l’IA dont Edward Witten est membre, a réclamé la publication sans délai des sorties en langage naturel et en Lean, la formalisation étant achevée selon OpenAI.
Comprendre et créditer, un travail confié à des bénévoles
Les auteurs de l’hypothèse refusent de certifier
Pour l’informatique, l’examen revient à Russell Impagliazzo et Ramamohan Paturi, de l’université de Californie à San Diego, deux des trois pères de l’ETH, et à Ryan Williams, du MIT ; à leur demande, OpenAI a accepté de rendre publiques toutes les données brutes et de financer une conférence. Leur lettre ouverte prévient que leur participation « ne doit pas être prise pour une certification ». Ils veulent un examen ouvert, qui ne confère la propriété de l’effort à aucune entreprise ni à aucun groupe choisi, eux compris, redoutent que la reconnaissance aille à qui publie le premier ou dispose des outils les plus puissants plutôt qu’à qui vérifie et explique, et proposent une réunion virtuelle avant la fin de 2026.
Le procès des mathématiciens désignés
La veille de l’annonce, l’AGMAI dénonçait sur le blog de Terence Tao les « mathématiciens désignés » qui reçoivent avant les autres les sorties des modèles : accès inégal, choix opaque, réputation empruntée qui protège l’entreprise de la critique. OpenAI admet que le choix des premiers « bergers » crée une asymétrie d’information et affiche ses principes : aucun accord de confidentialité, aucun crédit académique revendiqué, reconnaissance due aux groupes pour ce qu’ils comprennent et rédigent, participation bénévole. Renoncer au crédit n’est pas renoncer au bénéfice : l’annonce a coïncidé avec le lancement de GPT-6.1 Terra.
Les trois résultats n’ont pas le même statut : un manuscrit public et formalisé sans lecteurs désignés pour les ondes, une réfutation revendiquée par deux laboratoires, formalisée avec des écarts avoués et soumise aux auteurs mêmes de l’hypothèse, une physique qui n’existe publiquement que par la parole d’OpenAI. La vérification formelle écarte les erreurs de déduction ; elle ne dit ni ce qu’un résultat signifie ni ce qu’il change.
Si les machines trouvent, le travail rare devient de lire, de comprendre et de valider ce qu’elles trouvent. L’AGMAI rappelait le 29 septembre qu’un auteur comprend, vérifie et assume son argument ; les manuscrits du jour sont signés « OpenAI » et « Claude, Anthropic ». L’explication repose sur des bénévoles, comme ceux du dépôt oai-math-revised, présenté le 24 octobre pour réviser des manuscrits d’OpenAI jugés difficiles à suivre et mal sourcés, un travail gratuit au profit d’une entreprise lucrative, selon des commentateurs.
La réunion proposée avant la fin de l’année et la conférence promise diront si la complexité fine doit rebâtir ses fondations sur d’autres conjectures, ou si une faille surgit dans la traduction formelle. En physique, tout dépend du texte attendu du groupe Gross, ou de la publication que réclame l’AGMAI. La médaille Fields de juillet récompensait une compréhension de la dimension 3 ; la revendication d’octobre porte sur toutes les dimensions et attend ses lecteurs.
Aller plus loin
Le point de départ reste la publication d’OpenAI, Working with academic communities to build scientific understanding, qui expose les trois résultats, les trois stratégies de diffusion et les quatre principes affichés, dont le renoncement à tout crédit académique, et date les découvertes et les formalisations.
Le texte de la réfutation se lit dans The Exponential Time Hypothesis is False, dont l’introduction recense les bornes conditionnelles qui perdent leur fondement et celles qui survivent grâce à la conjecture des vecteurs orthogonaux, avant de détailler la méthode algébrique.
La question de la fidélité se pose sur pièces dans la fiche de formalisation Lean 378, qui énonce la borne effectivement démontrée, plus faible que celle du manuscrit, pour des formules encodées de façon canonique, et renvoie au fichier soumis à l’outil Comparator.
Le versant analytique tient dans Local smoothing for the Euclidean wave equation, dont l’introduction retrace l’histoire du problème, du théorème de Bourgain sur les moyennes circulaires aux travaux de Guth, Wang et Zhang, et liste les conséquences revendiquées pour Kakeya, Nikodym et la restriction de Fourier.
Le point de comparaison humain se trouve dans Volume estimates for unions of convex sets, and the Kakeya set conjecture in three dimensions, les 127 pages déposées sur arXiv le 24 février 2025 par Hong Wang et Joshua Zahl, qui ont réglé la dimension 3 et valu en juillet la médaille Fields à Hong Wang.
La version d’Anthropic, A 2^o(n) Time Algorithm for 3-SAT, vaut par sa déclaration de provenance, qui date la découverte et chiffre les jetons consommés, par son recensement des articles dépendant de l’ETH et par ses ordres de grandeur, qui montrent pourquoi un résultat théoriquement majeur reste sans portée pratique.
Pour refaire soi-même la vérification, le projet eth du dépôt anthropics/formal-math donne les commandes de compilation, les axiomes attendus et le rôle de Comparator et du second noyau nanoda, et reconnaît qu’aucune machine ne contrôle la correspondance entre l’énoncé formel et le papier.
La position des examinateurs s’exprime dans le Message to the TCS Community on ETH, où Russell Impagliazzo, Ramamohan Paturi et Ryan Williams refusent que leur nom vaille certification, réclament un examen ouvert à tous et posent la question du crédit dû à la vérification.
La critique la plus argumentée du dispositif est Disadvantages of Designating Mathematicians for AI Output Releases, publiée par l’AGMAI la veille de l’annonce, qui oppose au modèle des lecteurs choisis des règles de dépôt, de divulgation et de financement indépendant.
La part revendiquée en physique se mesure à l’aune de l’énoncé officiel du problème de Yang-Mills, rédigé par Arthur Jaffe et Edward Witten pour le Clay Mathematics Institute, qui exige à la fois l’existence d’une théorie quantique non triviale sur l’espace-temps à quatre dimensions et le trou de masse.
De la prépublication au fichier Lean, de la lettre des examinateurs à l’énoncé du Clay, ces pièces montrent une vérification formelle qui change la nature de la question sans la clore. Les machines produisent des preuves que des logiciels certifient, mais la fidélité des énoncés, le sens des méthodes et la portée des résultats restent l’affaire de lecteurs humains, dont le temps, le nombre et l’indépendance deviennent la ressource rare. Reste à savoir qui les choisit, qui les finance et qui sera crédité de leur travail.