La conjecture d’Aaronson et Ambainis, en suspens depuis 2008, est maintenant un théorème. Ce résultat provient d’un système de recherche interne développé par Physical Superintelligence (PSI) qui a utilisé un modèle d’IA propriétaire. La preuve, qui répond à une question fondamentale sur les limites des ordinateurs quantiques, a été acceptée par Lean, un assistant de preuve qui vérifie chaque étape mécaniquement.

Ce travail vient trancher une interrogation majeure de la théorie de la complexité : les ordinateurs quantiques peuvent-ils surpasser les machines classiques sur des problèmes dont l’entrée est aléatoire ? Les algorithmes quantiques connus, comme celui de Shor, tirent leur avantage exponentiel d’une structure interne présente dans les données. La conjecture posait l’inverse : si une telle structure n’est pas garantie, le gain exponentiel est-il possible ? Aaronson et Ambainis ont traduit cette question en un énoncé mathématique concernant les polynômes de faible degré.

L’idée centrale repose sur la notion d’influence. Si l’on considère un polynôme dont les valeurs restent comprises entre 0 et 1, la conjecture stipulait que si ce polynôme varie suffisamment selon les entrées (c’est-à-dire si sa variance est supérieure à un certain seuil $\varepsilon$), alors il doit exister au moins une variable dont le changement d’état affecte significativement sa valeur moyenne. C’est ce qu’on appelle l’« influence » d’une variable.

La mécanique de la preuve assistée par IA

La validation de cette conjecture repose sur la capacité des systèmes d’intelligence artificielle à traiter des domaines mathématiques d’une grande complexité. Selon PSI, leur système de recherche, qui employait un modèle Anthropic confidentiel, a abouti à une preuve complète en seulement trois jours de calcul. Ce résultat a ensuite été soumis à Lean, qui examine chaque étape de manière automatique et rigoureuse.

Les développements s’appuient sur des travaux antérieurs, notamment ceux de Shachar Lovett et Jiapeng Zhang. Le raisonnement avance par plusieurs étapes, incluant l’établissement d’inégalités complexes. Une des techniques utilisées passe par l’obtention d’une inégalité de type « tous les couples de points » à partir d’une affirmation sur les termes de plus bas degré dans le déterminant d’une matrice de monômes, comme le détaille la documentation de GitHub.

Pour ceux qui plongent dans les détails formels, le dépôt GitHub présente les déclarations Lean, telles que aaronson_ambainis et aaronson_ambainis_explicit. La conjecture initiale prévoyait une borne de l’ordre de $(\varepsilon/d)^7$. Une version explicite, ExplicitBound, utilise une borne plus précise : $(8\sqrt{15} / (125 \pi^4)) · \varepsilon^{5/2} / d^6$. Il existe aussi une version améliorée, ExplicitBoundImproved, qui intègre une hypothèse issue d’un article d’Agarwal et Ben-David, modifiant la constante de cette borne.

| Comparaison des bornes (Approximation) | :— | :— | :— | | Conjecture initiale | $(\varepsilon/d)^7$ | Borne attendue | | :— | | Borne explicite (PSI) | $(8\sqrt{15} / (125 \pi^4)) · \varepsilon^{5/2} / d^6$ | Borne prouvée | | :— | | Borne améliorée | $(32\sqrt{15} / (125 \pi^4)) · \varepsilon^{5/2} / d^6$ | Borne ajustée | | :— |

Implications pour les limites du calcul

Si cette preuve est acceptée, elle signifie que les ordinateurs quantiques ne peuvent pas, en théorie pure, réaliser des accélérations exponentielles sur des tâches dont les entrées sont distribuées de manière totalement aléatoire. Pour que ce gain colossal se produise, le problème doit obligatoirement posséder une structure mathématique exploitable par l’algorithme quantique.

Ce résultat vient compléter les travaux réalisés en août 2026 par Guy Blanc, Jordan Docter, Carmen Strassle et Li-Yang Tan de Stanford. Ces chercheurs avaient déjà prouvé l’absence de gain exponentiel pour une classe spécifique d’algorithmes quantiques examinant leur entrée par un nombre fixe d’itérations parallèles. Les chercheurs de Stanford ont commenté la preuve de PSI : « C’est un résultat énorme. Il résout une conjecture vieille de plusieurs décennies avec des implications importantes pour la nature des problèmes qui admettent des accélérations quantiques » (selon les chercheurs de Stanford, cités par PSI).

Le fait que la preuve ait été produite par des modèles d’IA, mais validée par Lean, souligne un point : même si l’IA est l’instrument de la découverte, le contrôle humain, via la vérification formelle, reste la garantie de la validité mathématique de l’avancée. Il faut désormais suivre si cette preuve passera par un processus de révision par les pairs conventionnel, car, comme le souligne le dépôt, elle n’a pas encore subi ce contrôle académique standardisé.

Sources

• GitHub – physical-superintelligence/aaronson-ambainis: A proof of the Aaronson-Ambainis conjecture, github.com
• A proof of the Aaronson-Ambainis conjecture, psi.inc
• Důkaz významné matematické domněnky o kvantových počítačích nalezen s pomocí AI, Root.cz, 9 novembre 2026
• Physical Superintelligence uses AI to crack a two-decade-old quantum computing puzzle, Crypto Briefing, 10 novembre 2026