PSI annonce une démonstration de la conjecture d’Aaronson-Ambainis vérifiée par ordinateur

Physical Superintelligence a annoncé le 6 novembre 2026 qu’un système de recherche interne, exécutant des instances d’un modèle non public d’Anthropic, avait trouvé une démonstration de la conjecture d’Aaronson-Ambainis, un problème d’informatique quantique ouvert depuis 2008.

Le système a produit une démonstration complète au cours du troisième jour d’une exécution sur l’infrastructure propre de PSI, et l’assistant de preuve Lean l’a acceptée. PSI a ensuite soumis au système des problèmes ouverts connexes, qui a amélioré le résultat à deux reprises avant que Lean n’accepte la version finale. Le manuscrit et la formalisation en Lean 4 sont publics.

Ce que la conjecture nous apprend sur les accélérations quantiques

La question est de savoir dans quels cas les ordinateurs quantiques peuvent être exponentiellement plus rapides que les machines classiques. L’algorithme de factorisation de Shor, datant de 1994, repose sur une structure : son entrée comporte un motif répétitif que l’algorithme peut exploiter. Le résultat de PSI porte sur le cas opposé, celui des entrées aléatoires ou dépourvues de structure, où un tel motif est généralement absent.

Dans le modèle de requête, un algorithme classique lit un bit par requête, tandis qu’une requête quantique peut être répartie en superposition sur plusieurs positions de l’entrée. L’explication de PSI relie ce modèle aux polynômes : après T requêtes quantiques, la probabilité que l’algorithme réponde oui est un polynôme borné des bits d’entrée, de degré au plus 2T. Simuler l’algorithme quantique revient donc à estimer ce polynôme sans lire un nombre exponentiel de bits d’entrée.

Dans leur article d’origine, Scott Aaronson et Andris Ambainis ont conjecturé que tout polynôme borné de faible degré possède une variable ayant une forte influence. Ils ont démontré que, si cette conjecture est vraie, tout algorithme quantique à T requêtes peut être simulé, pour la plupart des entrées, par un algorithme classique effectuant un nombre de requêtes polynomial en T. Il en découle que le nombre de requêtes classiques augmente de façon polynomiale, et non exponentielle, pour toute erreur d’approximation fixée et toute fraction d’entrées exclues ; cela n’exclut pas les avantages quantiques exponentiels pour les problèmes présentant une structure adéquate.

Formellement, le dépôt considère un polynôme réel p de degré au plus d, dont les valeurs sur le cube discret sont comprises entre 0 et 1. Si sa variance sur une entrée choisie uniformément au hasard est au moins égale à ε, une coordonnée présente une influence d’au moins (8√15 / (125π⁴)) · ε^(5/2) / d⁶, et donc d’au moins (ε/d)⁷. L’influence correspond à la variation quadratique moyenne de p lorsqu’on inverse le bit de cette coordonnée.

Comment la démonstration a été construite et vérifiée

La démonstration suit un plan de Shachar Lovett et Jiapeng Zhang fondé sur les certificats fractionnaires et les ensembles de niveau, mais remplace par une nouvelle inégalité portant sur toutes les paires une inégalité que leur plan laissait à l’état de conjecture. Un déterminant permet de construire un appariement bijectif des configurations d’entrée. Selon PSI, cet appariement va plus loin que celui, plus faible, du lemme du papillon de David Reimer, car il limite aussi la fréquence à laquelle les configurations appariées concordent sur chaque coordonnée, une borne nécessaire à la nouvelle inégalité.

Le dépôt divise la démonstration élémentaire en quatre parties : déduire l’inégalité portant sur toutes les paires à partir du déterminant et de la bijection, l’intégrer sur les ensembles de niveau, effectuer une moyenne sur les coordonnées et établir une borne sur les lignes à l’aide d’une borne ponctuelle de sensibilité. Ensemble, ces étapes donnent la borne explicite sur l’influence.

Selon l’audit consigné dans le dépôt, le développement formel ne contient aucun emplacement réservé à une preuve ni aucun axiome ajouté. Les déclarations ont été vérifiées à nouveau au moyen du noyau de Lean et de lean4lean, une implémentation indépendante du vérificateur de types de Lean. Lors d’une exécution en environnement isolé, un comparateur utilisant les noyaux de nanoda et de Lean a accepté les quatre théorèmes finaux ; sur une seconde machine, il a accepté une petite solution correcte et en a rejeté quatre délibérément erronées.

Ces vérifications comportent des limites explicites. Le lecteur doit encore confirmer que l’énoncé formel correspond à la conjecture publiée. L’article en langage naturel n’est pas lui-même vérifié par ordinateur, tandis que le noyau et le compilateur de Lean, les définitions de Mathlib et les machines utilisées pour les vérifications font toujours partie de la base de confiance.

Rôle des humains et examen par des experts

David Turturean, membre du personnel technique de PSI, a développé et exécuté le système de recherche, défini le périmètre du problème, demandé au modèle de préparer une première version, relu cette version et assume la responsabilité de l’exactitude de l’article. Le dépôt indique que les modèles d’IA ont produit les énoncés mathématiques, la première version et la formalisation Lean. Jim Halverson a audité la démonstration, et Phiala Shanahan a formulé des commentaires sur la formalisation.

L’annonce fait suite à un article soumis le 19 août 2026 par Guy Blanc, Jordan Docter, Carmen Strassle et Li-Yang Tan. Ces auteurs avaient établi la conséquence relative à la simulation classique pour les algorithmes quantiques parallèles, en démontrant qu’un algorithme à t requêtes et d tours peut être simulé sur la plupart des entrées au moyen de t^(O(d²)) requêtes classiques. PSI indique que les quatre auteurs ont lu l’intégralité de la démonstration, formulé des commentaires et préparent une présentation plus courte à l’intention des experts.

Dans leur évaluation publiée par PSI, les chercheurs ont écrit : « C’est un résultat majeur. Il résout une conjecture vieille de plusieurs décennies, aux importantes implications pour la nature des problèmes qui admettent des accélérations quantiques. La preuve s’appuie sur plusieurs axes de recherche en analyse des fonctions booléennes et en combinatoire probabiliste, qu’elle prolonge. Tout cela est réuni d’une manière presque magique. »

Le test immédiat est particulièrement concret : des noyaux de vérification indépendants peuvent rejouer l’argument encodé, mais des experts doivent encore confirmer que l’énoncé encodé correspond bien à la conjecture d’Aaronson et Ambainis et évaluer les parties de l’article qui ne sont pas formalisées dans Lean. Cette répartition détermine ce que les vérifications effectuées par la machine permettent d’établir et ce qui nécessite encore un examen mathématique humain.