PSI : une preuve Lean de la conjecture Aaronson-Ambainis trouvée par un système IA

Physical Superintelligence (PSI) a annoncé le 6 novembre 2026 qu’un système de recherche interne, alimenté par des instances d’un modèle Anthropic non public, a trouvé une preuve de la conjecture Aaronson-Ambainis, ouverte depuis 2008. Selon le laboratoire, Lean a accepté une preuve complète le troisième jour de la course, puis deux améliorations. Le manuscrit et la formalisation Lean 4 sont publics.

Ce que dit la conjecture

Scott Aaronson et Andris Ambainis se demandaient si un ordinateur quantique peut répondre à une question oui/non sur une chaîne aléatoire avec exponentiellement moins de lectures qu’un ordinateur classique. La plupart des accélérations spectaculaires connues (comme l’algorithme de Shor) reposent sur une structure rare dans l’entrée. Leur conjecture de mathématiques pures, si elle est vraie, implique qu’en l’absence de telle structure, le surcoût classique reste au plus polynomial en le nombre de lectures quantiques.

Concrètement, après T lectures, la probabilité qu’un algorithme quantique dise « oui » est un polynôme de degré au plus 2T à valeurs dans [0, 1]. La conjecture affirme qu’un tel polynôme, s’il varie assez, a toujours une variable d’influence suffisamment grande — ce qui permet à un ordinateur classique d’imiter la prédiction en ne regardant que peu de bits.

Ce que PSI publie

La page de recherche et le dépôt GitHub décrivent une preuve qui suit un plan de Lovett et Zhang, en remplaçant une inégalité qu’ils laissaient ouverte. Le README affirme quatre théorèmes Lean sans placeholder ni axiome ajouté, re-vérifiés par deux implémentations du noyau Lean (versions 4.33.0 / Mathlib v4.33.0, licence Apache 2.0). David Turturean a dirigé le travail ; Jim Halverson a audité la preuve ; Phiala Shanahan a commenté la formalisation.

En août 2026, quatre chercheurs de Stanford (Blanc, Docter, Strassle, Tan) avaient déjà réglé un cas particulier. PSI indique qu’ils lisent désormais la preuve complète et préparent une exposition plus courte ; le laboratoire cite un commentaire élogieux de leur part.

Limites à garder en tête

Le dépôt laisse au lecteur le soin de vérifier que l’énoncé Lean PrintedConjecture correspond bien à la conjecture imprimée. Un théorème amélioré s’appuie sur une hypothèse d’Agarwal et Ben-David non formalisée ici. Le papier en prose n’est pas vérifié par machine. Le modèle Anthropic n’est ni nommé ni public : on peut inspecter le résultat, pas rejouer la découverte. Aucune réaction publique d’Aaronson ou Ambainis n’a été trouvée au moment de notre rédaction.