Un système automatisé résout en trois jours la conjecture quantique d'Aaronson-Ambainis
La start-up de recherche en physique PSI utilise les modèles d'Anthropic et la vérification Lean pour s'attaquer à une question informatique vieille de 18 ans.
Traduit automatiquement de l’original en anglais Lire l’original
Un système de recherche computationnelle a généré une preuve mathématique formelle de la conjecture d'Aaronson-Ambainis, un problème ouvert vieux de 18 ans portant sur les limites de l'informatique quantique. L'entreprise de recherche en physique PSI a annoncé que sa plateforme automatisée avait produit la vérification en trois jours, recourant à l'intelligence artificielle pour déterminer quand les machines conventionnelles peuvent approcher les algorithmes quantiques.
Une limite vieille de 18 ans à l'avantage quantique
Proposée pour la première fois en 2008, la conjecture d'Aaronson-Ambainis explore les frontières exactes où les processeurs quantiques conservent un avantage de vitesse exponentiel sur les architectures numériques standard. Selon un article d'Interesting Engineering, la conjecture porte sur la question de savoir si les algorithmes quantiques présentant une structure mathématique spécifique peuvent être simulés par du matériel classique avec seulement un surcoût polynomial. Lorsque les machines classiques simulent des processus sur des entrées choisies au hasard dans des limites polynomiales, l'écart opérationnel apparent se réduit considérablement. Les procédures spécialisées établies telles que l'algorithme de Shor pour la factorisation des entiers restent inchangées par la conjecture, car la question mathématique concerne un sous-ensemble distinct de calculs quantiques.
Automatiser la preuve formelle avec Lean
Pour s'attaquer à la conjecture, le chercheur David Turturean a dirigé les travaux chez PSI, développant le flux de travail de recherche automatisé, formulant le problème computationnel et supervisant l'exécution. L'installation fonctionnait sur l'infrastructure interne de PSI, utilisant un modèle d'intelligence artificielle privé et non public développé par Anthropic. Lors de l'essai, la plateforme a produit des énoncés formels qui ont été chargés directement dans Lean, un assistant de preuve interactif conçu pour vérifier si les séquences logiques suivent strictement des axiomes mathématiques désignés. Le système a ensuite révisé l'argument à deux reprises, générant une version finale que Lean a acceptée sans incohérence logique.
Vérification indépendante et examen académique
La vérification formelle du code garantit la cohérence interne, mais les mathématiciens doivent encore établir que le théorème traduit correspond à la proposition originale de 2008. Le physicien Jim Halverson a audité la structure de la preuve, tandis que la physicienne théoricienne du MIT Phiala Shanahan a examiné la formalisation créée dans Lean. En parallèle, une équipe de recherche en mathématiques de l'université Stanford, composée de Guy Blanc, Jordan Docter, Carmen Strassle et Li-Yang Tan, a commencé à évaluer le résultat. Le groupe de Stanford, qui avait déjà démontré un cas particulier de la conjecture d'Aaronson-Ambainis en août 2026, rédige un article technique condensé pour expliquer les conclusions de PSI à la communauté scientifique au sens large.
Prochaines étapes pour la découverte scientifique automatisée
Le projet constitue une démonstration pratique de l'innovation en mathématiques assistées par machine de la part de PSI, une start-up lancée publiquement en septembre 2026 pour construire des moteurs de découverte autonomes. Si Lean fournit une validation programmatique de la logique, la preuve n'a pas encore achevé le processus standard d'évaluation par les pairs au sein de la communauté académique de physique. La diffusion future et l'examen par des théoriciens externes détermineront si la preuve résout pleinement la conjecture d'Aaronson-Ambainis.
