Le 10 novembre 2026, un comité présidé par David Gross, colauréat du prix Nobel de physique 2004, a rendu son avis sur une preuve produite par l’IA d’OpenAI et soumise le 28 octobre. Selon lui, cette preuve établit qu’une version quantique de la théorie de Yang-Mills en quatre dimensions peut être construite avec toute la rigueur mathématique. C’est la première des deux parties d’un problème du prix du millénaire de l’institut Clay.
La seconde partie, l’« écart de masse », une condition sur l’énergie minimale des états autres que le vide, n’est pas démontrée. Le prix de 1 million de dollars (environ 900 000 euros au cours de la BCE du 11 novembre 2026) n’est donc pas gagné. Dans son rapport de 35 pages, le comité écrit aussi : « Nous ne prétendons pas encore comprendre entièrement la preuve. »
La preuve examinée est écrite en Lean, un langage de programmation qui vérifie les démonstrations de façon mécanique. Cet avis est l’une de quatre annonces faites en 72 heures où un logiciel vérifie le travail d’une IA. Les trois autres concernent le dernier théorème de Fermat chez Anthropic, le code de la messagerie Signal chez Google DeepMind et un émulateur de services écrit par des agents d’IA chez AWS.
Un avis limité à l’existence de la théorie
La théorie de Yang-Mills est le type de théorie qui décrit l’interaction forte, la force qui lie les quarks à l’intérieur des protons et des neutrons. Sa version « pure », examinée ici, ne décrit que les gluons, les particules qui portent cette force.
En 2000, l’institut Clay a fait de sa construction rigoureuse l’un de ses sept problèmes du prix du millénaire, dans un énoncé rédigé par Arthur Jaffe et Edward Witten. Le magazine Scientific American y distingue deux parties : prouver que la théorie existe, puis prouver un « écart de masse ». Le comité définit ce dernier ainsi : tout état autre que le vide doit porter au moins une quantité d’énergie fixe et strictement positive.
Le 26 octobre, OpenAI a annoncé que ses modèles avaient produit le 9 septembre une preuve d’existence rédigée en langage courant, et qu’elle avait achevé une version en Lean le 16 octobre. Le même billet revendiquait une preuve pour la chromodynamique quantique (QCD), la théorie plus complète qui inclut les quarks. Il revendiquait aussi une réfutation de l’hypothèse du temps exponentiel, une conjecture d’informatique théorique : nous l’avions présentée à l’époque. Le 17 octobre, nous avions rapporté un autre résultat de physique obtenu par l’IA : des contre-exemples à une conjecture de 1967 sur la fusion.
David Gross a accepté de diriger le comité, un groupe chargé d’« accompagner » ce travail de physique. D’après Scientific American, il en a choisi lui-même les quatre autres membres : Michael Douglas, Arthur Jaffe (coauteur de l’énoncé du problème), Igor Klebanov et Nikita Nekrasov.
L’avis, ici traduit, se lit ainsi : « Selon nous, la soumission prouve qu’une théorie quantique des champs relativiste satisfaisant les axiomes de Wightman peut être construite comme limite d’échelle de la théorie de jauge de Wilson sur réseau en quatre dimensions, pour tout groupe de jauge compact simple. »
En termes simples, la preuve part d’une version de la théorie posée sur une grille de points, le réseau de Wilson, puis resserre cette grille sans fin. Elle montre que le résultat de ce passage à la limite, la « limite d’échelle », respecte les axiomes de Wightman, les règles de base d’une théorie quantique des champs relativiste.
L’avis ajoute que la soumission « ne prouve pas que la limite en volume infini est unique, ni qu’il existe un écart de masse ». L’unicité signifierait qu’une seule théorie peut sortir de la construction étendue à tout l’espace.
Une preuve de 9 477 fichiers passée au vérificateur
Lean contrôle chaque définition et chaque étape d’une preuve à l’aide d’un petit programme central, le noyau. Des chercheurs de Google s’en sont servis pour prouver que des programmes quantiques sont corrects dans un article soumis le 6 novembre.
Le comité a d’abord recompilé de zéro, dans Lean, les 9 470 modules d’OpenAI. L’opération a pris environ 184 minutes, sans aucune erreur. Les 9 477 fichiers source Lean correspondaient tous au manifeste de la soumission, la liste des fichiers qui l’accompagne.
Le code compte 250 319 déclarations, le terme de Lean pour les définitions, les théorèmes et les lemmes (résultats intermédiaires). Leur inventaire n’a trouvé ni axiome ajouté (un énoncé admis sans preuve), ni « sorry », le mot qui marque une étape laissée sans preuve. Le vérificateur fourni avec la soumission a ensuite repassé dans un noyau neuf les 100 168 déclarations dont dépendent les 17 résultats principaux. Les preuves n’utilisent que les trois axiomes standard de Lean.
Un second outil, Comparator, compare une preuve à une copie figée de l’énoncé visé et de ses définitions, la « cible », pour qu’un énoncé modifié ne puisse pas passer. Il a validé le théorème public d’OpenAI le 30 octobre.
Après avoir soumis sa preuve, OpenAI a signalé au comité que cette cible « omettait certains liens avec la construction sur réseau ». Le comité a rédigé une cible combinée plus exigeante, validée le 3 novembre. Il précise que son évaluation de ces liens « repose sur cette cible plus forte ».
Un noyau ne juge pas le sens des définitions. Selon le comité, son acceptation « ne permet pas de trancher si ces définitions expriment le problème visé, formulé en langage naturel ». Sa relecture humaine des définitions a été « étendue (mais pas exhaustive) ».
Le comité exprime aussi des « inquiétudes sur la qualité du code ». Seules 40 % des déclarations servent aux théorèmes principaux. Certains noms sont « peu conventionnels », comme Farewell.dead dans un fichier baptisé TicketsChart.lean.
Trois autres résultats vérifiés par la machine la même semaine
Le résultat de Google DeepMind porte sur un logiciel : le code cryptographique central de Signal. D’après son billet sur AlphaProof Code du 10 novembre, les chercheurs ont traduit avec plusieurs modèles d’IA les objectifs de sécurité de Signal en spécifications formelles, « chacune relue par des experts humains ». Une spécification formelle décrit en langage mathématique ce que le code doit garantir.
Pour prouver que le code respecte ces spécifications, des agents fondés sur Gemini Carbon, un modèle d’IA de Google, ont ensuite écrit « plus de six millions de lignes de Lean ». Les agents ont signalé « à peine 1 % du code » pour un second regard humain. Selon DeepMind, le travail a pris quatre semaines, alors que cette tâche « prend historiquement des années à des équipes d’experts ».
Pour tester la méthode, l’équipe a réintroduit deux vrais bogues, corrigés depuis longtemps, dans une copie isolée du code. Les deux fois, le système a produit une preuve, vérifiée par la machine, que la version boguée n’était pas sûre. Ehren Kret, directeur technique de Signal, note que les vérifications formelles précédentes « portaient sur de plus petites parties du code ».
Le résultat d’Anthropic, qui conçoit les modèles d’IA Claude, concerne le dernier théorème de Fermat. Ses agents ont formalisé une version simplifiée de la preuve d’Andrew Wiles : ils l’ont réécrite en Lean pour qu’une machine puisse la vérifier. Une première formalisation, annoncée le 4 septembre, avait demandé 11 jours et 13 millions de lignes de Lean à une version de recherche de Claude.
Dans un billet du 9 novembre, que nous avons présenté le 10 novembre, Anthropic indique qu’une équipe de 1 000 agents a refait cette formalisation avec Fable 5.2, son nouveau modèle. Elle l’a fait « en seulement 30 heures, avec une intervention humaine minimale », pour une preuve sept fois plus courte que la première. Une note ajoutée le 11 novembre précise le point de départ des agents : une liste de 60 énoncés, une esquisse d’une phrase de la démarche et « 47 lemmes déjà prouvés lors de notre formalisation précédente ».
Chez AWS, la branche d’informatique en nuage d’Amazon, le contrôle par la machine s’applique à du code ordinaire. Publié le 11 novembre, AWS Emulator imite les services d’AWS sur l’ordinateur d’un développeur, et AWS dit qu’il en couvre plus de 200. Matthew Goldberg, ingénieur principal senior, écrit que « notre équipe n’a écrit ni relu aucune ligne du code ».
Les agents rédigent des tests à partir des descriptions publiques des API d’AWS, ses interfaces de programmation, et « vérifient chacun sur le vrai AWS avant de le soumettre ». Avant d’être fusionnée au code principal, chaque modification doit compiler et passer une revue de code par des agents, un contrôle de sécurité et un contrôle de fidélité. Le 12 novembre, le dépôt public du code comptait 29 684 commits, les modifications enregistrées une à une. Le soir même, après sa dernière mise à jour, il en comptait 30 681, tous signés par des identités automatiques.
Les limites reconnues et les critiques
L’avis sur Yang-Mills ne couvre que l’existence de la théorie. Parmi les questions ouvertes, le comité cite l’unicité de la limite en volume infini et l’écart de masse. Les revendications d’OpenAI sur la QCD et sur une extension du modèle standard, la théorie de référence des particules élémentaires, n’ont ni fichiers publics ni avis. L’évaluation par le comité d’une deuxième soumission d’OpenAI, datée du 4 novembre, est notée « en cours ».
Comparator a tourné sous macOS sans isolation des processus, c’est-à-dire sans cloisonner les programmes entre eux. Ces essais ne testaient donc pas l’intervention d’un code malveillant au moment de la compilation. Aucune implémentation indépendante du noyau, un second vérificateur écrit séparément, n’a été utilisée.
La méthode suscite aussi des critiques. OpenAI a demandé à Gross de diriger le groupe. Pour assimiler le code, le comité s’est aidé d’Astra, le modèle d’IA d’OpenAI : c’est son « seul lien avec OpenAI » en dehors de la réception des soumissions, écrit-il.
Scientific American juge le document « trop sommaire pour donner une compréhension approfondie » du fonctionnement de la preuve. Le magazine note que cette méthode contredit les recommandations de transparence d’un groupe consultatif lié à OpenAI. Scott Armstrong, mathématicien à l’université de New York, lui a déclaré : « Cet examen peut se faire plus efficacement et plus vite en public. »
Sur Signal, le magazine Wired, repris par le site Ars Technica, relève que DeepMind n’a par exemple pas vérifié formellement l’application mobile dans son ensemble. DeepMind est aussi parti avec une longueur d’avance, grâce aux travaux de vérification antérieurs de Signal.
La documentation d’AWS Emulator exclut les « charges de travail de production », c’est-à-dire l’usage pour de vrais services en exploitation. Les agents consignent ce qui manque dans un dossier nommé things-that-do-not-work (« ce qui ne marche pas »).
Notre analyse
Sur Yang-Mills, la vérification par la machine a avancé bien plus vite que la compréhension humaine. Le billet d’Anthropic de septembre rappelle que la preuve du théorème de Fermat publiée par Andrew Wiles en 1995 faisait 129 pages et a « exigé des mois de travail minutieux pour être vérifiée ». La recompilation complète du code Yang-Mills a pris environ 184 minutes, et Comparator a validé la cible d’OpenAI deux jours après l’arrivée du code. Treize jours après l’avoir reçu, le comité ne prétendait toujours pas comprendre entièrement la preuve.
Le travail humain se déplace vers la question posée à la machine. Le comité a consacré la première partie de son rapport à comparer un à un les énoncés Lean aux exigences de Jaffe et Witten. Les experts de DeepMind ont relu chaque spécification. Dans le Guardian du 13 novembre, un logicien d’Helsinki a décrit une étape semblable dans le travail de Claude sur les carnets de Gödel : environ 200 des 663 théorèmes relevés ont dû être réparés pour le vérificateur Coq, énoncé précisé ou hypothèse ajoutée.
Swami Sivasubramanian, d’AWS, écrit sur le blog de Werner Vogels, directeur technique d’Amazon, que le métier de l’ingénieur consiste désormais à « construire les spécifications, les tests et les points de contrôle de fusion qui décident quand ce travail est correct ». Le risque restant se situe à cette étape : une cible peut omettre une propriété importante, comme l’a fait la première cible Yang-Mills d’OpenAI.
Les prochaines étapes sont l’avis du comité sur la soumission d’OpenAI du 4 novembre, d’éventuels documents publics sur la QCD et le travail de mathématiciens extérieurs sur le code Lean, désormais public. DeepMind dit publier ses fichiers de vérification de Signal en source ouverte.
Sources
- Validation of the OpenAI Yang-Mills construction, Yang-Mills group (présidé par David J. Gross), GitHub, 10 novembre 2026
- Working with academic communities to build scientific understanding, OpenAI, 26 octobre 2026
- Introducing AlphaProof Code: a breakthrough in verifying complex software at depth, Pushmeet Kohli et Swarat Chaudhuri, Google DeepMind, 10 novembre 2026
- Introducing Claude Fable 5.2 and Claude Mythos 5.2, Anthropic, 9 novembre 2026 (modifié le 11 novembre)
- Formalizing Fermat’s Last Theorem, Anthropic, 4 septembre 2026
- How we built the agents that built AWS Emulator, Matthew Goldberg, Amazon, 11 novembre 2026
- OpenAI’s ‘shepherds’ affirm blockbuster physics result, Joseph Howlett, Scientific American, 11 novembre 2026
- Google DeepMind just mathematically verified key parts of Signal, Lily Hay Newman (Wired), Ars Technica, 11 novembre 2026
Image d’en-tête : graphique MACCUS, données du Yang-Mills group (10 novembre 2026), de Google DeepMind (10 novembre 2026), d’Anthropic (4 septembre et 9 novembre 2026), d’AWS (11 novembre 2026) et de GitHub (12 novembre 2026)
