OpenAI soumet trois preuves d’IA à l’examen d’experts

OpenAI soutient que ses modèles ont obtenu trois résultats ambitieux : l’existence de certaines théories quantiques des champs en quatre dimensions, une preuve qui ferait tomber l’ETH en informatique, et la résolution d’une conjecture de lissage local en toutes dimensions avec des corollaires. L’entreprise a publié les données, recodé des preuves en Lean et mandaté des chercheurs pour arbitrer leur validité. Plusieurs protagonistes préviennent toutefois que ces affirmations exigent un contrôle indépendant et que certains volets, comme l’écart de masse en Yang-Mills, ne sont pas traités.

Physique : existence en 4D revendiquée, l’écart de masse reste ouvert

OpenAI affirme que son IA a établi l’existence mathématique de certaines théories quantiques des champs en quatre dimensions, un type de preuve qu’aucun travail n’avait encore réussi pour des théories avec particules en interaction. Le résultat est positionné sur les fondations de la physique des particules, domaine où la théorie quantique des champs, qualifiée par l’entreprise de cadre majeur, offre des prédictions très précises sans base mathématique pleinement rigoureuse. Les physiciens recourent à des approximations, comme des réseaux de points affinés, et la question demeure de savoir si ces procédures conduisent à une théorie unique et cohérente au sens mathématique, indépendamment de sa fidélité à la nature. La construction annoncée s’articule en étapes. D’abord la théorie de Yang-Mills, qui ne décrit que des gluons sans quarks et figure parmi les sept Millennium Prize Problems dotés chacun d’un million de dollars. Le problème associe la démonstration d’existence de la théorie et la preuve d’un écart de masse ; OpenAI précise ne traiter que la partie existence, si bien que le problème du Millénium ne serait pas intégralement résolu. Le paradoxe de portée de la force forte est rappelé : bien que les gluons soient sans masse dans les équations — comme la lumière pour l’électromagnétisme qui agit à grande distance —, la force forte ne s’exerce qu’à très courte portée, ce que la communauté explique par la formation de structures efficaces qui ont une masse, définissant un écart de masse encore non prouvé mathématiquement mais soutenu par des simulations. La deuxième étape est la chromodynamique quantique, qui ajoute les quarks et vise une description complète de la force forte. Selon OpenAI, l’existence mathématique de Yang-Mills et de la QCD découlerait principalement de la liberté asymptotique, l’affaiblissement de l’interaction à courte distance gardant les calculs maîtrisables même quand le réseau est raffiné. La troisième étape serait normalement le Modèle Standard, qui couvre trois des quatre forces fondamentales hors gravité, mais OpenAI indique qu’il ne peut pas être étendu à des dimensions arbitraires.

Procédure d’examen : pas de NDA, données diffusées, experts mandatés

Ryan Williams, avec Russell Impagliazzo et Ramamohan Paturi (UC San Diego), conduit une vérification indépendante et un travail d’explication. Il précise que le trio n’a signé aucun accord de confidentialité, n’est pas rémunéré et publiera des résultats intermédiaires, tout en soulignant que leur implication ne vaut pas validation et qu’un tel dossier exige un examen attentif. À la demande de ce groupe, OpenAI a mis en ligne les données brutes, y compris les écritures de preuves et leurs versions Lean, et s’est engagé à financer une conférence dédiée aux implications. L’entreprise dit adapter son dispositif selon les disciplines et avoir recodé des preuves en Lean, un langage qui permet une vérification pas à pas par ordinateur. Cette vérification n’exclut pas l’erreur, car elle ne porte que sur l’énoncé tel qu’il est formalisé ; des experts restent nécessaires pour confirmer que la formalisation capture bien le problème visé. Pour la conjecture de lissage local, aucun groupe de supervision n’est en place : OpenAI explique avoir consulté un expert externe et, sur son conseil, publié directement texte et preuve Lean pour que la communauté choisisse ses modalités de contrôle. OpenAI indique également mobiliser des spécialistes externes pour l’ensemble des vérifications.

Complexité : ETH donnée comme fausse et conséquences sur les circuits

Le pan informatique cible l’Exponential Time Hypothesis, hypothèse selon laquelle le pire cas de SAT demeure exponentiel avec l’ajout de variables. Cette position affine la frontière entre P et NP en quantifiant la difficulté de SAT. Même si ETH tombait, P pourrait rester différent de NP et les problèmes réputés difficiles ne deviendraient pas automatiquement faciles. L’hypothèse était largement admise et sert de pilier à des centaines d’articles établissant des bornes conditionnelles. OpenAI affirme que son système a prouvé la fausseté d’ETH. Si cette démonstration tient, les travaux fondés sur ETH perdraient leur assise sans être ipso facto réfutés. Selon Ryan Williams, le maintien de ce résultat aurait des retombées en théorie des circuits : une certaine classe de problèmes exigeants n’admettrait pas de petits circuits, au sens où, en doublant la taille d’entrée, le nombre de portes ne pourrait pas rester borné par environ un doublement. En toile de fond, SAT est au cœur de P contre NP : la vérification d’une proposition est rapide, mais trouver une affectation qui satisfait la formule est difficile ; chaque variable double l’espace de recherche et, pour 100 variables, le nombre de cas atteint une taille à 31 chiffres.

SAT en pratique : solveurs à l’échelle et prudence sur des gains rapides

SAT occupe une place centrale dans l’ingénierie, avec des solveurs qui contrôlent des circuits intégrés et participent au test logiciel, souvent sur des instances comptant des millions de variables. Ces cas industriels sont en général bien plus abordables que les pires cas théoriques, si bien qu’une amélioration ciblant exclusivement le pire cas ne se traduirait pas automatiquement par des bénéfices sur le terrain. Ryan Williams appelle à la prudence : il estime qu’il est trop tôt pour dire ce que les développeurs verraient concrètement et juge seulement plausible l’hypothèse de progrès substantiels de la résolution pratique de SAT dans les 12 mois. Il ajoute qu’on pourrait tout aussi bien ne rien observer de tel et dit ne pas savoir.

Analyse harmonique : lissage local toutes dimensions et corollaires

Le résultat en mathématiques vise la conjecture de lissage local, formulée en 1991 par Christopher Sogge pour des ondes comme le son, la lumière ou les secousses sismiques. Elle postule que, si une concentration extrême peut se produire ponctuellement, la moyenne temporelle du phénomène est plus uniforme. Jusque-là, la preuve n’existait qu’en deux dimensions, grâce à un résultat obtenu en 2019 par Guth, Wang et Zhang. OpenAI soutient avoir produit une preuve valable en toute dimension, y compris pour les ondes dans l’espace et dans des espaces de dimension supérieure. L’entreprise affirme aussi que deux conjectures majeures en découleraient : la conjecture de Kakeya en géométrie et celle de restriction de Stein en analyse de Fourier, cette dernière étudiant la décomposition d’un signal en oscillations. La difficulté de Kakeya est illustrée par un résultat de 2025 de Wang et Zahl, limité à trois dimensions ; selon OpenAI, ces deux conjectures seraient résolues dans toutes les dimensions si le lissage local était acquis.