Un sistema automatizzato risolve in tre giorni la congettura quantistica di Aaronson-Ambainis
La startup di ricerca fisica PSI usa i modelli di Anthropic e la verifica con Lean per affrontare una questione informatica vecchia di 18 anni.
Tradotto automaticamente dall’originale inglese Leggi l’originale
Un sistema di ricerca computazionale ha generato una dimostrazione matematica formale della congettura di Aaronson-Ambainis, un problema aperto da 18 anni che riguarda i limiti del calcolo quantistico. L'azienda di ricerca fisica PSI ha annunciato che la sua piattaforma automatizzata ha prodotto la verifica in tre giorni, impiegando l'intelligenza artificiale per stabilire quando le macchine convenzionali possono approssimare gli algoritmi quantistici.
Un limite di 18 anni al vantaggio quantistico
Proposta per la prima volta nel 2008, la congettura di Aaronson-Ambainis esplora i confini esatti in cui i processori quantistici mantengono un vantaggio di velocità esponenziale rispetto alle architetture digitali standard. Secondo quanto riportato da Interesting Engineering, la congettura si concentra sulla possibilità che gli algoritmi quantistici caratterizzati da una specifica struttura matematica siano simulabili da hardware classico con un sovraccarico solo polinomiale. Quando le macchine classiche simulano processi su input scelti casualmente entro limiti polinomiali, il divario operativo apparente si riduce in modo significativo. Procedure specializzate consolidate come l'algoritmo di Shor per la fattorizzazione degli interi restano immuni dalla congettura, poiché la questione matematica riguarda un sottoinsieme distinto di calcoli quantistici.
Automatizzare la dimostrazione formale con Lean
Per affrontare la congettura, il ricercatore David Turturean ha guidato il lavoro presso PSI, sviluppando il flusso di ricerca automatizzato, formulando il problema computazionale e supervisionando l'esecuzione. L'allestimento girava sull'infrastruttura interna di PSI, usando un modello di intelligenza artificiale privato e non pubblico sviluppato da Anthropic. Durante la prova, la piattaforma ha prodotto enunciati formali caricati direttamente in Lean, un assistente di dimostrazione progettato per verificare se le sequenze logiche seguono rigorosamente determinati assiomi matematici. Il sistema ha poi rivisto l'argomentazione due volte, generando un output finale che Lean ha accettato senza discrepanze logiche.
Verifica indipendente e revisione accademica
Il controllo formale del codice garantisce la coerenza interna, ma i matematici devono comunque stabilire che il teorema tradotto corrisponda alla proposizione originale del 2008. Il fisico Jim Halverson ha verificato la struttura della dimostrazione, mentre la fisica teorica del MIT Phiala Shanahan ha esaminato la formalizzazione creata in Lean. In parallelo, un gruppo di ricerca matematica della Stanford University composto da Guy Blanc, Jordan Docter, Carmen Strassle e Li-Yang Tan ha iniziato a valutare il risultato. Il gruppo di Stanford, che aveva già dimostrato un caso speciale della congettura di Aaronson-Ambainis in agosto 2026, sta redigendo un articolo tecnico sintetico per spiegare le scoperte di PSI alla più ampia comunità scientifica.
I prossimi passi della scoperta scientifica automatizzata
Il progetto rappresenta una dimostrazione pratica dell'innovazione nella matematica assistita dalle macchine da parte di PSI, una startup lanciata pubblicamente in settembre 2026 per costruire motori autonomi di scoperta. Mentre Lean fornisce una validazione programmatica della logica, la dimostrazione non ha ancora completato la revisione paritaria standard presso la comunità accademica della fisica. La futura diffusione e la revisione da parte di teorici esterni determineranno se la dimostrazione risolve del tutto la congettura di Aaronson-Ambainis.
