Physical Superintelligence (PSI), un laboratoire de recherche américain, a annoncé le 6 novembre une preuve de la conjecture d'Aaronson-Ambainis, un problème central de l'informatique quantique ouvert depuis 2008. Un système interne, fondé sur un modèle Anthropic non public et un harnais développé par David Turturean, a produit la preuve en trois jours de calcul. Le papier et la formalisation complète en Lean 4 sont publics sur GitHub. Le vérificateur accepte la preuve sans axiome ajouté ni trou.
- Un système de PSI fondé sur un modèle Anthropic non public a produit une preuve de la conjecture d'Aaronson-Ambainis, publiée le 6 novembre avec sa formalisation Lean 4 sur GitHub.
- Lean garantit la chaîne logique, pas l'énoncé : la correspondance entre la définition formelle et la conjecture d'origine tient en une quinzaine de lignes, encore à confirmer par des spécialistes.
- La même semaine, le benchmark FrontierPhysics montre que les meilleurs agents échouent à plus de 70 % des tâches de recherche en physique. Le théorème bien posé reste le cas favorable pour l'IA.
Ce que Lean a vérifié, et ce qu'il n'a pas vérifié
Scott Aaronson et Andris Ambainis ont posé la conjecture dans un papier mis en ligne en 2009. Elle affirme que tout polynôme borné de bas degré sur le cube booléen possède une variable influente. Un algorithme quantique qui fait T requêtes correspond à un polynôme de degré au plus 2T, un résultat classique du domaine. Le théorème interdit donc toute accélération quantique superpolynomiale sur des entrées sans structure particulière. Shor et les menaces sur RSA ne sont pas concernés : ils exploitent précisément une structure.
La première preuve obtenue donnait un exposant de 22, que le système a ensuite ramené à 7. La borne finale garantit une influence d'au moins 0,0025 fois ε^(5/2)/d⁶. Le noyau de Lean, lean4lean et un troisième vérificateur indépendant ont rejoué la formalisation, bâtie sur Lean 4.33. Le replay séquentiel prend 11 minutes et 7,4 Go de RAM : n'importe qui peut le refaire sur un portable.
Le papier lisible, lui, n'est pas vérifié machine. Le quatrième théorème dépend d'un résultat d'Agarwal et Ben-David jamais formalisé. Surtout, rien ne prouve mécaniquement que la définition Lean « PrintedConjecture » dit la même chose que la conjecture d'origine. Cette correspondance tient en une quinzaine de lignes, à relire par les bonnes personnes. Ni Aaronson ni Ambainis n'avaient réagi au 7 novembre. Le domaine a déjà connu une fausse joie : en 2019, Keller et Klein avaient publié une preuve humaine de la même conjecture, rétractée après la découverte d'une faille.
Quatre chercheurs de Stanford (Blanc, Docter, Strassle, Tan), qui avaient prouvé un cas particulier en août, parlent d'un « résultat énorme » et relisent la preuve complète. C'est au moins le troisième résultat mathématique majeur attribué à l'IA en quelques semaines. En octobre, Scott Aaronson relevait déjà sur son blog la preuve de la conjecture Unique Games et la réfutation de l'hypothèse du temps exponentiel.
Mon avis : notable, pas encore un basculement. Tant que des spécialistes n'ont pas confirmé les quinze lignes d'énoncé, la preuve reste une revendication très solide, pas un théorème accepté. Le vrai signal pour les équipes françaises est la méthode. Un modèle frontier plus un vérificateur formel produit des résultats auditables en 11 minutes. Les sorties libres d'un agent, elles, restent invérifiables.
La recette qui marche : un vérificateur externe, pas un meilleur prompt
Ce résultat concerne les équipes qui confient à un LLM des tâches où l'erreur coûte cher : code critique, calcul, extraction de données. L'IA a réussi ici parce qu'un vérificateur mécanique tranchait à chaque étape. Lean joue pour la preuve le rôle que jouent les tests et le typage pour le code.
Le contre-exemple est sorti deux jours avant. FrontierPhysics, un benchmark publié le 4 novembre par 42 physiciens, teste 22 modèles sur 56 tâches de recherche, de la revue de littérature au manuscrit final. Aucun agent ne dépasse 30 % de réussite. L'analyse manuelle des échecs pointe la rigueur du raisonnement et le jugement d'expert, pas le code ni les connaissances. Sans vérificateur externe, l'agent fait illusion.
Les laboratoires gardent aussi en interne des modèles plus capables que ceux de leurs API. Anthropic n'a pas nommé le modèle utilisé par PSI, comme OpenAI réserve l'accès à son modèle classé « Critical ». Si vous comparez des modèles sur les benchmarks publics, vous mesurez la génération d'avant.
- Clone le dépôt « aaronson-ambainis » de Physical Superintelligence, puis lance make check et make replay : la vérification séquentielle tient en 11 minutes et 7,4 Go de RAM.
- Ouvre Conjecture.lean et compare la définition PrintedConjecture à la conjecture 1.7 du papier d'Aaronson et Ambainis : toute la confiance repose sur cette quinzaine de lignes.
- Parcours les 56 tâches de FrontierPhysics (arXiv 2611.06910) avant de confier un projet de recherche entier à un agent : le meilleur modèle échoue presque trois fois sur quatre.
Sources
- GitHub - physical-superintelligence/aaronson-ambainis, preuve et formalisation Lean (6 novembre 2026)
- Quentir - PSI's Lean 4 Proof of the Aaronson-Ambainis Conjecture (7 novembre 2026)
- Qelvin - An AI Proved a Quantum Conjecture. The Same Week, AI Agents Failed Most Physics Research Tasks (novembre 2026)
- Interesting Engineering - Major quantum computing conjecture solved in three days after 18 years (novembre 2026)
- arXiv - FrontierPhysics : un benchmark de recherche en physique pour les agents (4 novembre 2026)
- Shtetl-Optimized - le blog de Scott Aaronson (novembre 2026)
Source : Github.com
Cet article a été rédigé avec l’assistance d’un modèle de langage (LLM).
