PSI: una dimostrazione Lean della congettura di Aaronson-Ambainis trovata da un sistema IA
Physical Superintelligence annuncia che un sistema di ricerca interno, basato su un modello Anthropic non pubblico, ha trovato una dimostrazione della congettura di Aaronson-Ambainis (2008), accettata da Lean 4. Il manoscritto e la formalizzazione sono pubblici.
Physical Superintelligence (PSI) ha annunciato il 6 novembre 2026 che un sistema di ricerca interno, alimentato da istanze di un modello Anthropic non pubblico, ha trovato una dimostrazione della congettura di Aaronson-Ambainis, aperta dal 2008. Secondo il laboratorio, Lean ha accettato una dimostrazione completa al terzo giorno di esecuzione, seguita poi da due miglioramenti. Il manoscritto e la formalizzazione in Lean 4 sono pubblici.
Cosa afferma la congettura
Scott Aaronson e Andris Ambainis si chiedevano se un computer quantistico potesse rispondere a una domanda sì/no su una stringa casuale con un numero esponenzialmente inferiore di letture rispetto a un computer classico. La maggior parte delle accelerazioni spettacolari note (come l’algoritmo di Shor) si basa su una struttura rara nell’input. La loro congettura di matematica pura, se vera, implica che in assenza di tale struttura il sovraccarico classico rimanga al massimo polinomiale rispetto al numero di letture quantistiche.
Concretamente, dopo T letture, la probabilità che un algoritmo quantistico risponda «sì» è un polinomio di grado al massimo 2T con valori in [0, 1]. La congettura afferma che un tale polinomio, se varia a sufficienza, possiede sempre una variabile di influenza abbastanza grande — il che consente a un computer classico di imitare la previsione esaminando solo pochi bit.
Cosa pubblica PSI
La pagina di ricerca e il repository GitHub descrivono una dimostrazione che segue uno schema di Lovett e Zhang, sostituendo una disuguaglianza che questi ultimi avevano lasciato aperta. Il README certifica quattro teoremi in Lean senza placeholder né assiomi aggiunti, riverificati da due implementazioni del kernel di Lean (versioni 4.33.0 / Mathlib v4.33.0, licenza Apache 2.0). David Turturean ha guidato il lavoro; Jim Halverson ha supervisionato la dimostrazione; Phiala Shanahan ha commentato la formalizzazione.
Nell’agosto 2026, quattro ricercatori di Stanford (Blanc, Docter, Strassle, Tan) avevano già risolto un caso particolare. PSI indica che stanno ora leggendo la dimostrazione completa e preparando un’esposizione più sintetica; il laboratorio riporta un loro commento elogiativo.
Limiti da tenere a mente
Il repository lascia al lettore l’onere di verificare che l’enunciato in Lean PrintedConjecture corrisponda effettivamente alla congettura stampata. Un teorema migliorato si basa su un’ipotesi di Agarwal e Ben-David non formalizzata qui. Il testo dell’articolo non è verificato dalla macchina. Il modello Anthropic non è né nominato né pubblico: si può esaminare il risultato, ma non replicare il processo di scoperta. Nessuna reazione pubblica di Aaronson o Ambainis era stata registrata al momento della nostra redazione.
La nostra lettura
Il segnale non è che «un modello ha inventato la teoria dei numeri», ma che un sistema di ricerca affiancato a un verificatore formale è oggi in grado di produrre un artefatto esaminabile su un problema aperto da diciotto anni. La macchina propone, Lean convalida una parte del lavoro, e l’essere umano resta responsabile della corrispondenza tra l’enunciato formalizzato e la congettura originale. Finché questa fedeltà e la peer review non saranno confermate, la reazione corretta è trattare il repository come una candidata dimostrazione verificata da macchina, e non come un teorema già acquisito nel canone.
Fonti
- PSI — A proof of the Aaronson-Ambainis conjecture (6 novembre 2026) Fonte primaria
- GitHub — physical-superintelligence/aaronson-ambainis (articolo + Lean 4) Fonte primaria
- Aaronson & Ambainis — The Need for Structure in Quantum Speedups (arXiv:0911.0996) Fonte primaria — Enunciato originale della congettura
Una fonte primaria proviene direttamente dall'azienda, dal laboratorio o dall'ente interessato. Una fonte secondaria riporta l'informazione senza esserne l'autrice: la segnaliamo come tale. Un errore? Consulta la nostra politica di rettifica.
