Conjecture d'Aaronson-Ambainis : une IA a prouvé en trois jours une énigme quantique vieille de 18 ans

Le 6 novembre, une petite entreprise appelée Physical Superintelligence (PSI) a annoncé quelque chose qui aurait ressemblé à de la science-fiction il y a dix ans : un système de recherche en IA, fonctionnant sur un modèle non public d'Anthropic, avait prouvé la conjecture d'Aaronson-Ambainis, un problème ouvert central de la théorie de la complexité quantique qui tenait depuis 2008. Le système disposait d'une preuve complète dès le troisième jour de l'exécution. Lean, l'assistant de preuve qui vérifie chaque étape logique par machine, l'a acceptée. PSI a ensuite lancé le système sur des problèmes voisins, amélioré le résultat à deux reprises, et publié à la fois un article et la formalisation publique en Lean, afin que chacun puisse revérifier le travail.

Pour comprendre pourquoi cela compte, commençons par ce dans quoi les ordinateurs quantiques sont réellement bons. En 1994, Peter Shor a trouvé un algorithme quantique qui factorise les grands nombres bien plus vite que toute méthode classique connue. Mais l'accélération de Shor repose sur un don rare : le problème cache un motif répétitif, et l'ordinateur quantique trouve à quelle fréquence il se répète. La plupart des accélérations quantiques spectaculaires connues fonctionnent de la même façon. Elles exploitent la structure.

Scott Aaronson et Andris Ambainis ont posé la question gênante : qu'en est-il des entrées aléatoires, qui n'ont presque jamais cette structure ? Un ordinateur quantique peut-il répondre à une question par oui ou par non sur une chaîne aléatoire en lisant les bits exponentiellement moins de fois qu'un ordinateur ordinaire ? Ils ont énoncé une conjecture sur les polynômes — des mathématiques pures — et montré que, si elle est vraie, la réponse est non : sur des entrées aléatoires, les ordinateurs quantiques sont au plus polynomialement plus rapides. La conjecture est devenue l'un des problèmes ouverts centraux de la théorie de la complexité quantique, et en août 2026, un groupe de Stanford l'a prouvée pour un cas particulier : les algorithmes quantiques qui lisent leur entrée en un nombre fixe de rondes parallèles.

La preuve de PSI suit un plan tracé par Shachar Lovett et Jiapeng Zhang, en remplaçant une inégalité que leur plan laissait comme conjecture par une nouvelle inégalité prouvée dans le manuscrit, au moyen d'un argument d'appariement fondé sur le lemme du papillon de David Reimer et sur des résultats de plusieurs autres groupes. L'humain dans la boucle, David Turturean de PSI, a construit le système de recherche, délimité le problème, l'a exécuté et assume la responsabilité de l'exactitude de l'article. Le conseiller Jim Halverson a audité la preuve. Le groupe de Stanford qui a prouvé le cas particulier lit la preuve complète, a envoyé des commentaires et rédige une exposition plus courte pour les experts. Leur verdict pour l'instant : « C'est un résultat énorme. »

C'est la bonne façon de lire cette histoire — non comme un couronnement, mais comme une affirmation accompagnée d'un artefact vérifiable. L'acceptation par Lean est une barre haute : une machine a vérifié chaque étape de l'argument. Ce que Lean ne peut pas vérifier, c'est si l'énoncé formel est bien l'énoncé qui intéresse les mathématiciens, ou si la formalisation introduit en douce une hypothèse cachée. C'est le travail des experts humains, et il est encore en cours. L'évaluation par les pairs n'a pas eu lieu. Le modèle qui a trouvé la preuve n'est pas public, donc personne ne peut relancer la découverte elle-même — seulement inspecter ce qu'elle a produit.

Et c'est là que la semaine où cette annonce est tombée devient la vraie histoire. La preuve de PSI n'est pas un événement isolé. En octobre, OpenAI a publié 722 manuscrits mathématiques rédigés par IA, dont des preuves revendiquées de l'hypothèse quasi-Riemann, de la conjecture des jeux uniques et de la conjecture de Hodge pour une classe particulière de formes. En septembre, un article du Quarterly Journal of Mathematics a rapporté qu'un système d'IA avait trouvé l'idée clé qui transformait des résultats conditionnels sur les k-différentielles en théorèmes inconditionnels, avec le lemme crucial formellement prouvé en Lean. Axiom a formalisé le Stacks Project, d'environ 7 500 pages — quelque 16 millions de lignes — rendant un immense corpus de géométrie algébrique vérifiable par machine. Le motif est désormais sans équivoque : l'IA propose, et Lean dispose. Le goulot d'étranglement est passé de la découverte des preuves à leur vérification, et c'est là que les humains donnent encore le rythme.

C'est ce basculement que je surveille. Si l'exposition de Stanford aboutit proprement et qu'aucun groupe rival ne trouve de faille, la preuve d'Aaronson-Ambainis deviendra le deuxième grand résultat attribué à l'IA en un mois à survivre à l'examen des experts — et la question cessera d'être de savoir si l'IA peut faire des mathématiques de pointe pour devenir : à quelle vitesse le processus de vérification peut-il suivre ? Ma prédiction : d'ici le 31 décembre 2027, cette preuve aura été confirmée publiquement par des mathématiciens indépendants, par l'exposition du groupe de Stanford, une publication évaluée par les pairs ou une confirmation publique équivalente d'experts, sans qu'aucune faille matérielle ne soit trouvée. Je lui donne 65 % — la barre mécanique est déjà franchie, les bons experts sont déjà mobilisés, mais la confirmation humaine n'est pas une formalité, et un seul écart de définition peut encore faire échouer une preuve vérifiée par Lean.