En chimie, une molécule nouvelle se juge sur deux pièces : le produit, que tout laboratoire peut passer au spectromètre, et la voie de synthèse, publiée pour que d’autres la refassent ou la contestent. Un composé dont la recette reste secrète peut être authentique ; la discipline, elle, avance par les procédés qu’elle partage.
Les mathématiques échappaient à ce dédoublement, puisque lire une démonstration revient à en refaire chaque pas. Les systèmes d’intelligence artificielle qui démontrent le réintroduisent : leurs annonces se succèdent en 2026 à un rythme inédit, et l’art de trouver tient dans un logiciel et un modèle que leurs détenteurs gardent pour eux.
Le 6 novembre, la vague atteint la complexité quantique. La société américaine Physical Superintelligence, ou PSI, dit avoir démontré la conjecture d’Aaronson-Ambainis, qui résistait depuis 2008, avec un système maison où opérait un modèle d’Anthropic anonyme et non public. L’assistant de preuve Lean a validé la déduction ; aucun spécialiste extérieur n’a encore publié son évaluation. Restent à examiner l’acteur, la question de 2008, les garants et contrôles de la preuve, sa portée et le crédit quand la méthode échappe.
Une jeune société et un modèle sans nom
Établie à Cambridge, dans le Massachusetts, PSI a le statut de public benefit corporation, une société à mission d’intérêt public, et se veut un laboratoire de physique fondé sur l’IA, où travailleraient des « virtual physicists ». Lancée le 1er septembre, elle a levé 58 millions de dollars d’amorçage, un tour mené par Breakthrough Energy Ventures selon Glitchwire. Elle conçoit le système, pas les modèles : ses cinq résultats du 23 octobre en information quantique créditaient des modèles d’OpenAI et d’Anthropic ; cette fois, l’exécution n’a mobilisé qu’un modèle d’Anthropic non public.
Selon PSI, le système a bouclé une preuve complète dans son troisième jour de calcul, validée par Lean. Le manuscrit publié sur GitHub décrit des instances du modèle qui fouillaient la littérature, avançaient des idées, les croisaient et les éprouvaient, quand d’autres encadraient ce travail et leurs échanges.
Cette première preuve se contentait d’une borne médiocre, d’exposant 22. Lancé ensuite par PSI sur des questions ouvertes connexes, à partir de ses acquis intermédiaires, le système a ramené l’exposant à 11 en intégrant sur les niveaux, puis à 7 en moyennant sur les coordonnées, chaque version repassant par Lean. L’annexe A du manuscrit, seule fenêtre sur la méthode, montre le modèle exhumant d’abord l’inégalité de Reimer, puis prouvant ses idées dans un autre ordre que celui où il les avançait.
La question posée en 2008
La structure, moteur de l’avantage quantique
Peter Shor a montré en 1994 qu’un ordinateur quantique décomposerait d’immenses entiers en facteurs premiers bien plus vite que les méthodes classiques connues, grâce à une période cachée que la mesure quantique fait ressortir. Les grandes accélérations reposent presque toutes sur une telle régularité, une promesse faite sur l’entrée. Restait le cas des données tirées au hasard : un gain exponentiel y était-il possible ? Nul ne savait le dire.
Des requêtes aux polynômes
Scott Aaronson, de l’université du Texas à Austin, théoricien de l’informatique, et Andris Ambainis, de l’université de Lettonie, ont ramené la question à un énoncé sur les polynômes ; Aaronson l’exposait dès 2008 lors d’une conférence, et leur article commun sur le besoin de structure a paru en 2014 dans Theory of Computing. Ils s’appuient sur un lemme de Beals et de ses coauteurs, publié en 2001 : pour un algorithme qui consulte t fois son entrée, la probabilité de répondre oui s’écrit comme un polynôme de degré au plus 2t, compris entre 0 et 1. Selon la conjecture, dès que ce polynôme varie assez, l’une de ses variables est influente : la basculer change vraiment la valeur.
Sur le cube booléen, pour un degré d et une variance d’au moins ε, l’influence de cette variable doit atteindre une puissance fixe de ε/d, quand les meilleures bornes générales s’effondraient exponentiellement avec le degré ; PSI annonce (ε/d)⁷. Si le résultat tient, une machine classique peut estimer, avec une faible erreur, la probabilité qu’un algorithme quantique réponde oui sur presque toutes les entrées aléatoires, en un nombre de lectures polynomial en t, et non exponentiel.
Une tentative retirée, un cas réglé
Le 9 novembre 2019, Nathan Keller et Ohad Klein déposaient une démonstration qu’Aaronson saluait ; le 2 décembre, ils la retiraient, leur lemme 5.3 ne prouvant pas ce qu’il affirmait, précédent qui commande la prudence actuelle. En août 2026, Guy Blanc, Jordan Docter, Carmen Strassle et Li-Yang Tan, de Stanford, réglaient dans une prépublication attendue à FOCS 2026, qui s’ouvre le 8 novembre à New York, le cas où les requêtes se font en un nombre fixe de rondes parallèles. PSI revendique le cas général en suivant le plan tracé en 2022 par Shachar Lovett et Jiapeng Zhang ; son manuscrit montre au passage qu’une inégalité qu’ils avaient conjecturée est fausse telle qu’énoncée, et la remplace.
Un auteur, des relecteurs et des silences
Le manuscrit ne porte qu’un nom, celui de David Turturean, qui a chez PSI le titre de member of technical staff. Il a choisi le problème, conçu puis lancé le système, a fait rédiger un premier jet par une instance du modèle, a relu ce texte et s’en porte personnellement garant ; le README du dépôt attribue à des modèles d’IA les énoncés, ce brouillon et la formalisation. Parmi les conseillers de PSI, Jim Halverson a audité la démonstration et Phiala Shanahan, physicienne théoricienne au MIT, a commenté sa formalisation en Lean. Anthropic n’est créditée ni par le manuscrit ni par PSI comme autrice ou collaboratrice.
À Stanford, les quatre chercheurs étudient la preuve et préparent pour les spécialistes un exposé plus ramassé. Selon PSI, seule source de ces propos, leur lettre s’ouvre sur « this is a huge result » et juge presque magique la façon dont la preuve fait converger des pistes de recherche distinctes. Le manuscrit remercie Aaronson de leur avoir adressé PSI, mais son avis public manque au 7 novembre : le dernier billet de son blog, du 5 novembre, traite d’autre chose, et Ambainis ne s’est pas exprimé publiquement.
Ce que Lean certifie, et ce qu’il laisse aux humains
Quatre contrôles pour une déduction
Dans Lean, un noyau compact, le kernel, contrôle chaque inférence. Le dépôt contient une formalisation en Lean 4 adossée à la bibliothèque Mathlib et quatre théorèmes finaux, sans aucun sorry, la balise qui signale une étape non prouvée, ni axiome ajouté : #print axioms n’y fait apparaître que les trois axiomes usuels. Un seul théorème repose sur un résultat d’Agarwal et Ben-David non formalisé ; le principal, aaronson_ambainis, s’en passe. La preuve est rejouée par leanchecker, par Lean4Lean, dit indépendant par le README mais dérivé, selon son propre dépôt, du noyau en C++ dont il peut partager des bogues, puis par nanoda, vérificateur indépendant écrit en Rust, via l’outil comparator.
Vingt lignes à confronter au texte imprimé
Le théorème principal vise une définition, PrintedConjecture, qui tient en une vingtaine de lignes et ne recourt qu’à des objets de Mathlib : tout polynôme réel dont le degré total ne dépasse pas d, compris entre 0 et 1 aux sommets du cube et dont la variance atteint ε, a une variable d’influence au moins (ε/d)⁷. Le fichier problem_statement.md la met en regard de la conjecture imprimée, qui ne fixait pas l’exposant. Le code est publié sous licence Apache 2.0, le manuscrit de 60 pages appartient à son auteur ; la lecture ne demande qu’un navigateur, et make check ou make replay relancent les contrôles avec Lean 4.33.0 et Mathlib.
Le README reconnaît lui-même deux angles morts : la définition correspond-elle à la conjecture imprimée, et le texte, écrit pour des humains, est-il juste ? Qu’elle dévie de l’original, et le théorème, toujours vrai, porterait sur une autre question ; au 7 novembre, aucun spécialiste étranger à PSI n’a publié cette confrontation. Conséquences, historique, panorama de la preuve et remarques finales restent hors de la formalisation, aucun examen par des pairs n’est encore engagé et, d’ici l’exposé de Stanford, seul l’auteur garantit l’exactitude du texte.
Une frontière pour le calcul quantique
Une limite en lectures, qui épargne Shor
Le résultat porte sur les consultations de l’entrée, ou requêtes, pas sur la durée du calcul. Il ne dit pas qu’un ordinateur classique imite tout calcul quantique et laisse ouverte la question de BPP face à BQP, les problèmes que résolvent en temps raisonnable une machine classique munie de hasard et un ordinateur quantique. Même en requêtes, la simulation reste théorique : pour approcher avec une erreur η la probabilité d’acceptation d’un algorithme à t requêtes, sauf sur une fraction δ des entrées, le manuscrit garantit au plus (4t)⁸·η⁻¹⁴·δ⁻⁸ requêtes, une borne qui dépasse 10⁵⁶ pour dix requêtes et des tolérances d’un pour cent.
Rien là ne rend les ordinateurs quantiques inutiles ni ne touche la factorisation de Shor, dont l’entrée est promise périodique : le résultat écarterait seulement un gain exponentiel en requêtes sur des entrées aléatoires, pour des questions fermées, sans rien dire de la durée totale ni du matériel réel. Pour The Quantum Insider, il invite à chercher les gains exponentiels dans des problèmes structurés, sans indiquer quelles applications en tireront un bénéfice concret. Les machines suivent leur propre voie, des qubits réinitialisés du Nighthawk R2 d’IBM aux travaux de Claude Mythos 5 sur les circuits quantiques.
Un exposant qui n’est pas un optimum
Le manuscrit ne présente pas l’exposant 7 comme optimal : la conjecture exigeait une borne polynomiale, ce que (ε/d)⁷ fournit. Sa section 9 recense ce qui reste ouvert, de l’exposant de la variance, qui ne pourra pas descendre sous 2, au rôle inévitable du degré, et la bijection au cœur de la preuve attend une construction combinatoire directe. La descente de 22 à 11 puis à 7 dans une même exécution suggère une marge, pas un plafond.
Une mathématique devenue cadence
Le 20 mai, un modèle interne d’OpenAI réfutait la conjecture d’Erdős sur les distances unités ; le 20 juillet, Levent Alpöge annonçait un contre-exemple à la conjecture jacobienne trouvé avec Claude Fable 5 ; le 2 août, OpenAI attribuait à une version interne de son modèle dix résultats certifiés en Lean 4 ; le 26 octobre, elle en revendiquait trois, dont la réfutation de l’hypothèse du temps exponentiel, qu’Anthropic revendiquait le lendemain par une autre voie. Claude avait aussi résolu une conjecture de percolation, GPT-6 Astra Pro trouvé des contre-exemples à celle de Grad, et OpenAI revendiqué des avancées sur deux problèmes du millénaire.
Le crédit sans la recette
Le cas de PSI pousse à l’extrême la question du crédit : la preuve se contrôle mieux que bien d’autres, sa fabrication pas du tout. Le modèle reste anonyme et inaccessible, le système ne sort pas de PSI, le dépôt ne compte qu’une révision : nul ne peut rejouer les trois jours d’exécution. La déclaration de Leiden des mathématiciens, publiée le 2 juin, exige auteur humain, divulgation et, le cas échéant, vérification formelle, et critique la diffusion par communiqué ; PSI en suit la lettre, mais a d’abord publié sur une page d’entreprise, qui tient déjà la conjecture pour un théorème.
Ce qui tranchera
Le verdict tient à deux points circonscrits, ce qui pourrait le hâter face à d’autres revendications récentes : la fidélité de l’énoncé, qu’un spécialiste peut vérifier le temps d’une soirée, et l’examen du manuscrit par le groupe de Blanc, capable de se prononcer en quelques semaines. Si les deux tiennent, la conjecture de 2008 deviendra un théorème ; si l’énoncé s’écarte de l’original, Lean aura certifié une autre question, et celle de 2008 restera ouverte.
Une société lancée deux mois plus tôt revendique la solution, trouvée en trois jours, d’une question que la complexité quantique se posait depuis 2008, et une machine a contrôlé chaque inférence. Ce qui manque est précis : la certitude que vingt lignes de Lean disent ce que disait la conjecture, et une lecture extérieure des soixante pages.
Le travail humain se déplace plus qu’il ne disparaît : choisir le problème, construire le dispositif, relire, signer, et s’assurer que l’énoncé vérifié est le bon. Ce dernier geste devient le lieu de la confiance ; il exige des lecteurs qui comprennent la conjecture et le code, et aucune vérification formelle ne le remplace.
L’asymétrie de la chimie demeure : une preuve vérifiable dont la recette reste privée enrichit la discipline et sert de vitrine à son détenteur, ici une jeune société tournée d’abord vers les centres de données. Reste à dire ce que vaut un théorème dont nul ne peut refaire la découverte. Pour le calcul quantique, l’enjeu est plus sobre : si la preuve tient, l’avantage exponentiel en lectures exige une structure, et la quête d’applications garde son cap.
Aller plus loin
Le document central reste A proof of the Aaronson-Ambainis conjecture, le manuscrit de soixante pages signé par David Turturean : sa section de divulgation, son historique des bornes et son annexe A, qui suit pas à pas les idées du modèle, se lisent sans tout maîtriser, et sa section 9 dresse la liste des questions encore ouvertes.
L’annonce publiée par PSI le 6 novembre sous le même titre, A proof of the Aaronson-Ambainis conjecture, livre la version de l’entreprise : elle tient déjà la conjecture pour un théorème, détaille le rôle de chacun et cite plus longuement la lettre du groupe de Stanford, dont elle reste la seule source.
La question de la fidélité se juge sur pièce grâce à problem_statement.md, qui recopie la conjecture imprimée, place en regard les énoncés formalisés, explique le passage d’un cube à l’autre et donne chaque borne sous une forme sans racines : c’est le document qu’un expert extérieur doit confronter au texte de 2014.
L’article fondateur, The Need for Structure in Quantum Speedups, déposé dès 2009, énonce la conjecture et sa conséquence sur la simulation classique ; il contient aussi un second résultat souvent oublié : pour les problèmes invariants par permutation, comme la recherche de collisions, la complexité quantique en requêtes vaut au moins la racine septième de la complexité classique.
La méthode polynomiale sur laquelle tout repose vient de Quantum Lower Bounds by Polynomials, où Beals, Buhrman, Cleve, Mosca et de Wolf, dans un texte déposé en 1998, montrent que, sans promesse sur l’entrée, l’accélération quantique en requêtes reste au plus polynomiale, un constat que la conjecture prolonge aux entrées aléatoires.
Le cas déjà réglé des algorithmes à profondeur bornée est exposé dans Quantum Speedups Require Structure or Depth, prépublication déposée le 19 août par le groupe de Stanford qui relit la preuve de PSI : sans structure, un gain superpolynomial y exigerait une profondeur non constante, et un gain exponentiel une profondeur polynomiale.
La stratégie suivie se lit dans Fractional certificates for bounded functions, le rapport de Lovett et Zhang de juillet 2022, qui ramenait la conjecture à des énoncés plus maniables ; le manuscrit de PSI montre que la conjecture 37 de ce rapport, une extension de l’inégalité de Talagrand, est fausse telle qu’énoncée, puis la remplace.
Le précédent de 2019 est raconté par l’intéressé dans The Aaronson-Ambainis Conjecture (2008-2019), billet du 17 novembre 2019 où Aaronson explique l’enjeu en termes accessibles et dont la mise à jour consigne le retrait de la preuve de Keller et Klein, après la faille repérée par Paata Ivanisvili.
La chaîne de contrôle est décrite par la référence officielle du langage, Validating a Lean Proof, qui gradue les vérifications, de la simple compilation au passage par comparator, distingue la validité d’une preuve du sens de son énoncé et range les preuves d’IA non relues parmi les tentatives potentiellement malveillantes.
Le doute sur les définitions a un précédent instructif, raconté dans Definitions in the liquid tensor experiment, billet d’octobre 2022 où Adam Topaz présente les exemples ajoutés au Liquid Tensor Experiment, achevé en juillet sur un défi de Peter Scholze, pour que des lecteurs peu familiers de Lean vérifient ses définitions.
Lus ensemble, ces textes séparent l’acquis de ce qui reste à juger. La question remonte à 2008, ses outils à 1998, la stratégie à 2022 ; la vérification formelle apporte une garantie forte mais bornée à la déduction. Ce qui manque au 7 novembre tient en deux lectures extérieures, celle de l’énoncé et celle du manuscrit, et en une méthode que personne ne peut encore refaire.