OpenAI annonce trois preuves faites par IA : les experts doivent trancher

OpenAI affirme que ses modèles internes ont produit des preuves dans trois disciplines : mathématiques, informatique et physique. L’un de ces résultats toucherait à un problème du prix du millénaire. Mais l’entreprise n’annonce pas une victoire : elle fait appel à des experts extérieurs pour savoir si ces preuves tiennent. Tout ce qui suit est donc une revendication d’OpenAI, rapportée par The Decoder, et non un fait établi.

Ce qu’OpenAI affirme, et ce qu’elle ne dit pas

Selon The Decoder, OpenAI a détaillé trois résultats dans un article de blog. Elle dit que ses modèles internes ont produit les preuves. Elle qualifie les manuscrits de « sorte de données de recherche brutes », qu’il faut encore comprendre.

L’entreprise a donc demandé à des experts extérieurs de jouer le rôle de « bergers » (en anglais, shepherds) pour ces résultats. Chaque discipline est traitée différemment, d’après les conseils de ces experts. OpenAI précise aussi avoir traduit les preuves de maths et d’informatique en Lean.

Le média rapporte par ailleurs que l’un des résultats démontrerait une partie d’un des problèmes du prix du millénaire. Le lien exact entre ce résultat et le problème visé reste à établir par les spécialistes. Rien n’est validé à ce stade.

Deux précisions sur ce que l’article ne dit pas. Le prix Nobel apparaît dans le titre de The Decoder, sans plus de détail sur son identité ni son rôle. Quant au troisième résultat, en physique, The Decoder ne le décrit pas dans le texte que nous citons : nous ne le traiterons donc pas ici.

Le cas de l’informatique : une hypothèse centrale mise en cause

Le résultat le plus spectaculaire concerne l’hypothèse du temps exponentiel, ou ETH (Exponential Time Hypothesis). Elle porte sur le problème SAT : étant donné une formule logique dont les variables valent « vrai » ou « faux », peut-on les choisir pour que toute la formule soit vraie ?

Avec peu de variables, on teste toutes les combinaisons. Mais chaque variable supplémentaire double le nombre de cas. À 100 variables, on atteint un nombre à 31 chiffres.

L’ETH dit, en gros, qu’il n’existe pas de raccourci réel. On peut accélérer l’essai-erreur, mais dans le pire des cas, le temps de calcul explose à chaque variable ajoutée. L’hypothèse va plus loin que la célèbre conjecture « P différent de NP » : elle ne dit pas seulement que SAT est difficile, mais à quel point.

Selon OpenAI, son système aurait démontré que l’ETH est fausse. The Decoder précise qu’elle était largement admise. Des centaines d’articles en théorie des graphes, biologie computationnelle, bases de données ou géométrie algorithmique s’appuient dessus. Si la preuve tient, ces travaux perdraient leur fondement. Leurs résultats ne deviendraient pas automatiquement faux, mais ils ne seraient plus démontrés.

Attention aux raccourcis. Selon The Decoder, même si l’ETH tombait, P pourrait toujours différer de NP : les problèmes difficiles ne deviendraient pas faciles du jour au lendemain.

Un gain pratique incertain, un séisme théorique possible

SAT n’est pas qu’un exercice de logique. Des programmes spécialisés, les solveurs SAT, vérifient des puces électroniques ou testent des logiciels. Ils traitent déjà des formules de millions de variables, car les cas réels sont souvent bien plus simples que le pire cas visé par l’ETH. Accélérer le pire cas n’améliorerait donc pas forcément ces outils.

Le professeur du MIT Ryan Williams reste prudent sur X. Interrogé sur ce que les développeurs verraient en premier, il répond que personne ne le sait. Au rythme actuel, dit-il, des progrès sérieux sur la résolution pratique de SAT sont plausibles d’ici 12 mois. « Ou nous ne verrons rien de tel. Je ne sais vraiment pas », reconnaît-il.

Sur le plan théorique, l’effet serait plus net. Toujours selon Williams, si le résultat tient, une classe de problèmes très exigeants ne pourrait pas être résolue par de petits circuits logiques.

Une vérification confiée à ceux qui ont proposé l’hypothèse

Williams va examiner et expliquer le résultat de façon indépendante, avec Russell Impagliazzo et Ramamohan Paturi, de l’université de Californie à San Diego. Ces deux derniers ont proposé l’ETH avec Francis Zane. Autrement dit, ce sont les chercheurs mêmes qui ont formulé l’hypothèse que la preuve prétend réfuter qui la passent au crible.

Williams écrit que ce groupe n’a signé aucun accord de confidentialité, travaille bénévolement et partagera ses constats au fur et à mesure. La source ne dit rien de la rémunération des autres vérificateurs ou experts consultés.

Dans une lettre ouverte, les trois chercheurs précisent que leur implication ne vaut pas validation. Un résultat de cette ampleur exige, écrivent-ils, une revue indépendante et minutieuse. À leur demande, OpenAI publie toutes les données brutes, dont la preuve rédigée et la preuve en Lean. Elle s’est aussi engagée à financer une conférence sur les conséquences pour le domaine.

Lean ne suffit pas : qui vérifie l’énoncé ?

Lean est un langage qui permet à un ordinateur de contrôler chaque étape d’une preuve. Cela ne garantit pas l’absence d’erreur, précise The Decoder. Lean vérifie seulement que la preuve établit l’énoncé tel qu’il a été écrit en Lean. Reste à savoir si cet énoncé correspond bien au problème visé. Cette question-là, seuls des experts humains peuvent la trancher.

Le deuxième résultat, en mathématiques, illustre l’enjeu. Il porte sur la conjecture du lissage local, proposée en 1991 par le mathématicien Christopher Sogge. Elle décrit comment des ondes, comme le son, la lumière ou les secousses sismiques, se concentrent : cette concentration extrême ne dure que brièvement, et en moyenne les ondes se comportent de façon plus régulière.

Elle n’avait été prouvée qu’en deux dimensions, par Guth, Wang et Zhang en 2019. OpenAI dit que ses modèles la démontrent en toutes dimensions. Si c’est exact, deux autres conjectures célèbres en découleraient : celle de Kakeya, en géométrie, et celle de la restriction de Stein, en analyse de Fourier. Wang et Zahl n’avaient prouvé Kakeya qu’en dimension trois, en 2025.

Contrairement aux deux autres résultats, aucun groupe dédié n’accompagne cette preuve. OpenAI dit avoir contacté un expert extérieur pour discuter d’une telle collaboration. Sur son conseil, elle a publié le texte de la preuve et la preuve en Lean.

Ce que le lecteur peut en retenir

Cette annonce pose une question simple : que vaut une découverte avant qu’un humain compétent l’ait lue ? Ici, l’entreprise elle-même reconnaît que ses manuscrits sont de la matière première, pas un verdict.

Plusieurs points sont à surveiller :

• Les conclusions intermédiaires du groupe de Ryan Williams, qu’il promet de partager.
• La question de savoir si les énoncés écrits en Lean correspondent bien aux problèmes visés.
• Le sort de la preuve en mathématiques, qui n’a pas, pour l’instant, de groupe de vérification dédié.

Le même réflexe vaut à plus petite échelle. Un chiffre, un code ou une analyse produits par un modèle méritent un contrôle avant d’être utilisés, surtout si le coût d’une erreur est élevé. Si même une preuve accompagnée de son code de vérification doit être relue par les chercheurs mêmes qui ont formulé l’hypothèse qu’elle prétend réfuter, que devrait-on exiger d’un simple tableau de chiffres généré en dix secondes ?

Sources

• OpenAI asks outside experts, including a Nobel laureate, to check proofs its AI produced in math, computer science, and physics (The Decoder)