Le 6 novembre 2026, Physical Superintelligence (PSI) a affirmé que son système de recherche interne, utilisant un modèle Anthropic non public et non nommé, avait produit une preuve de la conjecture d’Aaronson–Ambainis acceptée par Lean. Dans son annonce, PSI présente ce résultat comme une avancée en complexité des requêtes quantiques. Son dépôt public en précise l’énoncé formel et ce que la vérification établit.

La conjecture porte sur les fonctions polynomiales qui dépendent d’entrées binaires. Elle est importante parce que PSI relie ces fonctions à la possibilité d’estimer, avec un algorithme classique, le comportement de certains algorithmes quantiques sur des entrées aléatoires.

L’énoncé formel porte sur l’influence d’un bit

Le dépôt Lean 4 de PSI considère un polynôme réel de degré au plus d, dont les valeurs restent entre 0 et 1 sur le cube booléen {0,1}^N, c’est-à-dire sur l’ensemble des entrées de N bits. Il suppose aussi que sa variance sous une entrée tirée uniformément est au moins ε, avec ε > 0.

L’influence d’un bit i mesure le changement moyen du polynôme quand on inverse ce bit, le changement étant mis au carré : Inf_i[p] = E_X[(p(X) − p(X^i))²]. Ici, X est une entrée uniforme et X^i la même entrée avec son bit i retourné.

Pour au moins une coordonnée, le dépôt énonce une borne inférieure d’influence égale à (8√15/(125π⁴))·ε^(5/2)/d⁶. Le coefficient devant le reste vaut environ 0,0025. Le dépôt présente également une formulation nommée PrintedConjecture, dans la normalisation de PSI, avec la borne (ε/d)^7.

Une preuve formelle porte d’abord sur l’énoncé effectivement codé ; vérifier que cet énoncé correspond à la conjecture visée demande aussi une lecture mathématique.

Ce que Lean vérifie, et la question qui reste à examiner

Le dépôt recense quatre déclarations finales de théorèmes Lean et indique que la formalisation ne contient ni placeholders ni axiomes ajoutés. Il rapporte aussi des vérifications avec le noyau de Lean et lean4lean. Ces contrôles vérifient que les propositions formalisées découlent de la logique de Lean.

Le dépôt précise toutefois que cette vérification ne décide pas si PrintedConjecture exprime bien la conjecture voulue. Il indique également que l’article rédigé pour des lecteurs humains n’est pas lui-même vérifié par machine. Lean, son compilateur et son noyau, les définitions de Mathlib et les machines de vérification font partie de la base de confiance décrite par le dépôt.

Dans son annonce du 6 novembre, PSI indiquait que Guy Blanc, Jordan Docter, Carmen Strassle et Li-Yang Tan, chercheurs à Stanford, lisaient la preuve et lui avaient transmis des commentaires.

La conséquence annoncée concerne le nombre de requêtes

En complexité des requêtes, une requête consiste à consulter une partie de l’entrée. PSI explique qu’après T requêtes quantiques, la probabilité qu’un algorithme réponde « oui » peut être représentée par un polynôme borné de degré au plus 2T. La conséquence que PSI associe à la conjecture est qu’un algorithme classique peut approximer cette probabilité en effectuant un nombre polynomial de lectures de l’entrée, pour la plupart des entrées aléatoires et avec une erreur et une proportion fixées.

Cette portée concerne le nombre de requêtes dans ce modèle précis. Elle ne donne pas une borne sur le temps total d’exécution de tout algorithme quantique.