Le 6 novembre 2026, la jeune entreprise de recherche PSI (Physical Superintelligence) a annoncé une démonstration de la conjecture d’Aaronson-Ambainis. Cette hypothèse sur les limites des ordinateurs quantiques était ouverte depuis 2008. Selon PSI, son système de recherche, qui faisait tourner un modèle d’IA d’Anthropic non public, tenait une preuve complète au troisième jour de calcul. Lean, un logiciel qui vérifie chaque étape d’une preuve, l’a acceptée.
Le jour même, PSI a mis en ligne l’article et la preuve formelle, écrite pour Lean, sur GitHub, un site de partage de code. Cette preuve compte 648 théorèmes vérifiés par la machine, sans étape laissée en suspens. Aucune revue scientifique n’a encore relu l’article.
Une question sur les limites des ordinateurs quantiques
Sur certains problèmes, un ordinateur quantique bat de très loin un ordinateur classique. En 1994, Peter Shor a trouvé un algorithme quantique qui décompose les grands nombres en facteurs premiers bien plus vite que toute méthode classique connue. Comme la plupart des accélérations spectaculaires, il repose sur une garantie : la donnée cache un motif qui se répète.
Les informaticiens Scott Aaronson et Andris Ambainis se sont demandé ce qui se passe sans cette garantie. Ils comptent les lectures : combien de fois une machine doit consulter sa donnée, une suite de 0 et de 1, pour répondre par oui ou non. Sur une donnée structurée, un ordinateur quantique peut la lire exponentiellement moins souvent qu’un ordinateur classique. Personne ne savait s’il en allait de même sur des suites tirées au hasard, presque toujours sans motif.
Ils ont ramené la question à des mathématiques pures. La probabilité qu’un algorithme quantique réponde oui s’écrit comme un polynôme des bits d’entrée, une formule faite de sommes et de produits de ces bits. Sa valeur reste entre 0 et 1.
Dans leur article, ils conjecturent que tout polynôme de ce type et de faible degré (peu de bits multipliés entre eux) a une variable « très influente ». C’est un bit dont l’inversion fait nettement bouger la valeur, en moyenne. Si c’est vrai, un ordinateur classique peut imiter l’ordinateur quantique sur la plupart des entrées en lisant d’abord les bits influents. L’écart de lectures reste alors polynomial, loin de l’écart exponentiel des données structurées.
Dix-huit ans de tentatives
Aaronson écrit qu’il n’a jamais réussi à résoudre cette question. « Vers 2008, j’ai remarqué qu’une solution découlerait d’une conjecture au lien peut-être pas évident », ajoute-t-il sur son blog Shtetl-Optimized. L’article de PSI relie ce constat à un exposé qu’il a donné cette année-là au centre de recherche de Banff. Le texte cosigné avec Ambainis est paru sur le site de prépublications arXiv le 5 novembre 2009, puis dans la revue Theory of Computing en 2014.
Aaronson raconte aussi que le problème a « pris une vie propre » chez les spécialistes des fonctions booléennes (des fonctions de bits). Ryan O’Donnell, Guy Kindler « et beaucoup d’autres » s’y sont essayés. Aaronson a même convaincu le mathématicien Terence Tao d’y consacrer « une heure ou deux ».
Le billet, daté du 17 novembre 2019, s’intitule « The Aaronson-Ambainis Conjecture (2008-2019) » : Nathan Keller et Ohad Klein avaient annoncé une preuve une semaine plus tôt. Ils l’ont retirée, indique une mise à jour en tête du billet. Paata Ivanishvili avait repéré ce qui « ressemble pour l’instant à une erreur fatale dans le lemme 5.3 », une étape intermédiaire de la preuve.
Le 19 août 2026, Guy Blanc, Jordan Docter, Carmen Strassle et Li-Yang Tan, de l’université Stanford, ont résolu le problème pour les algorithmes quantiques parallèles. Ces algorithmes lisent leur donnée en un nombre fixe de tours.
Le 28 septembre, Uma Girish, Kunal Mittal, Barak Nehoran et Ran Raz ont montré que plusieurs variantes de la question reviennent toutes au problème d’origine. Ces variantes tirent les entrées au hasard autrement. Les auteurs qualifient ce problème de « conjecture de longue date en théorie de la complexité quantique ».
Une preuve au troisième jour, puis deux améliorations
PSI a mené la recherche sur sa propre infrastructure, avec un système conçu par l’un de ses chercheurs, David Turturean. Selon la déclaration d’usage de l’IA en tête de l’article, plusieurs copies d’un même modèle d’Anthropic y travaillaient. Elles se partageaient les tâches : chercher des idées existantes, en proposer, les combiner et les tester, superviser l’ensemble.
D’après la chronologie publiée en annexe, la première preuve complète a été rédigée au troisième jour de calcul, puis vérifiée dans Lean. Cette version démontrait la conjecture avec une garantie faible. Dans la formulation d’origine, elle assurait au bit le plus influent une influence d’au moins (ε/d) puissance 22. Ici, ε mesure combien le polynôme varie et d est son degré.
La conjecture demande seulement une puissance fixe, et plus elle est petite, plus le résultat est fort. PSI a ensuite orienté les copies du modèle vers des problèmes ouverts voisins. En chemin, elles ont resserré le résultat deux fois, à la puissance 11 puis 7, et Lean a validé chaque version.
La preuve suit un plan de Shachar Lovett et Jiapeng Zhang, mais remplace l’inégalité qu’ils avaient laissée non démontrée par une inégalité nouvelle. Elle s’appuie aussi sur le lemme du papillon de David Reimer, tiré de sa preuve de la conjecture de van den Berg-Kesten publiée en 2000.
Des humains ont piloté le projet. Turturean a conçu le système, cadré le problème, lancé la recherche, fait rédiger au modèle un premier jet de l’article et relu ce texte. Il « est responsable de l’exactitude de l’article », précise PSI. Le conseiller Jim Halverson a audité la preuve, et la conseillère Phiala Shanahan a commenté les fichiers Lean.
Le 23 octobre, PSI avait déjà publié des résultats sur cinq problèmes ouverts de théorie de l’information quantique, obtenus avec son système de recherche en IA, dont au moins un partiel.
La part vérifiée par la machine
Dans Lean, un petit programme central, le noyau, doit valider chaque étape d’une preuve. La société Axiom Math a utilisé ce logiciel en octobre pour convertir une preuve de 15 000 pages en code vérifié par ordinateur.
Le dépôt GitHub de PSI compte 84 modules Lean et 761 déclarations, dont 648 théorèmes. Il n’ajoute aucun axiome, c’est-à-dire aucune affirmation admise sans preuve. Un audit automatique ne trouve aucun « sorry » dans le code de la bibliothèque, le mot qui signale dans Lean une preuve manquante.
Un vérificateur séparé, leanchecker, a fait repasser chaque déclaration par le noyau Lean. L’opération a été refaite avec lean4lean, une réécriture indépendante du vérificateur de types de Lean. L’outil Comparator a confronté les quatre théorèmes finaux à l’énoncé formel et les a fait revérifier par nanoda, un vérificateur écrit dans le langage Rust.
Le fichier de présentation du dépôt indique lui-même les limites de ces contrôles. Sa section « Trust boundary » (limite de confiance) laisse au lecteur un point à confirmer : l’énoncé formel dit-il bien ce que dit la conjecture ?
Cet énoncé est une courte définition nommée PrintedConjecture. Le fichier la reproduit en entier, et un fichier séparé la place à côté de l’énoncé original. L’article rédigé pour les lecteurs humains n’est, lui, pas vérifié par la machine.
Une annonce encore à confirmer
Presque tout ce qui précède vient de PSI : l’annonce, l’article et le code. L’article est une prépublication hébergée sur GitHub, sans relecture par une revue.
Le résultat sort du propre système de PSI, une public benefit corporation (forme américaine proche de la société à mission) financée par du capital-risque. Elle affiche plus de 58 millions de dollars levés.
L’avis de l’équipe de Stanford passe lui aussi par PSI, qui cite ces quatre chercheurs : « C’est un résultat majeur. Il résout une conjecture vieille de plusieurs décennies, avec des conséquences importantes sur la nature des problèmes qui admettent une accélération quantique. » Nous n’avons trouvé aucune déclaration de leur part sur leurs propres canaux.
L’article de PSI remercie Aaronson de l’avoir mise en relation avec cette équipe. Le matin du 7 novembre, le blog d’Aaronson ne contenait aucun billet sur la preuve.
La portée du résultat est aussi étroite. Il mesure les lectures de la donnée, pas le temps de calcul total, comme l’a relevé Matt Swayne sur le site spécialisé The Quantum Insider le 6 novembre. Il vaut pour des questions à réponse oui ou non et des entrées aléatoires : les problèmes structurés, comme la factorisation de Shor, ne sont pas concernés.
Swayne note encore que ce récit n’établit pas avec quelle régularité le système pourrait résoudre d’autres problèmes ouverts de longue date. Les chercheurs extérieurs peuvent examiner la preuve, mais pas relancer la recherche : le modèle n’est pas public.
Notre analyse
La preuve est arrivée au troisième jour d’un calcul, après 18 ans d’efforts humains. Le mode de vérification compte autant que la vitesse. La tentative de 2019 a échoué sur une erreur cachée dans une étape. Une preuve Lean revérifiée par des outils indépendants est conçue pour détecter ce genre de faille.
Il reste aux experts une vérification plus étroite : s’assurer qu’une courte définition formelle dit bien ce qu’Aaronson et Ambainis avaient en tête. Ils doivent aussi faire confiance à Lean, à sa bibliothèque mathématique et aux machines qui ont fait tourner les contrôles.
En octobre, OpenAI affirmait que son IA avait réfuté l’hypothèse du temps exponentiel, une conjecture d’informatique théorique. Anthropic disait aussi que son modèle Claude avait conçu des circuits quantiques jusqu’à 39 fois moins coûteux que les meilleurs publiés. Comme celle d’OpenAI, l’annonce de PSI arrive avec sa preuve formelle en accès libre.
Selon PSI, l’équipe de Stanford prépare une version courte de la preuve pour les spécialistes. Au 7 novembre, nous n’avons trouvé aucun commentaire public d’Aaronson ni d’Ambainis. PSI n’a pas dit si l’article sera soumis à une revue, ni quel modèle a mené la recherche.
Sources
- A proof of the Aaronson-Ambainis conjecture, PSI, 6 novembre 2026
- The Aaronson-Ambainis conjecture: paper and Lean 4 formalization, PSI sur GitHub, 6 novembre 2026
- The Need for Structure in Quantum Speedups, Scott Aaronson et Andris Ambainis, arXiv, 5 novembre 2009
- The Aaronson-Ambainis Conjecture (2008-2019), Shtetl-Optimized, 17 novembre 2019
- Quantum Speedups Require Structure or Depth, Guy Blanc, Jordan Docter, Carmen Strassle et Li-Yang Tan, arXiv, 19 août 2026
- Distributional Variants of the Aaronson-Ambainis Conjecture, Uma Girish, Kunal Mittal, Barak Nehoran et Ran Raz, arXiv, 28 septembre 2026
- Five results on Open Quantum Problems, PSI, 23 octobre 2026
- AI-Assisted Proof Settles Longstanding Question About Quantum Speedups, The Quantum Insider, 6 novembre 2026
Image d’en-tête : frise MACCUS, données d’Aaronson (Shtetl-Optimized, 2019), d’arXiv et de PSI (23 octobre et 6 novembre 2026)
