Il 6 novembre 2026 Physical Superintelligence (PSI) ha dichiarato che un suo sistema di ricerca, eseguito con un modello non pubblico di Anthropic non identificato, ha prodotto una prova della congettura di Aaronson–Ambainis accettata da Lean. Il repository pubblico di PSI precisa che cosa afferma la formalizzazione; spetta però ai lettori stabilire se l’enunciato formale corrisponde davvero alla congettura che si intendeva dimostrare. Nell’annuncio, PSI ha riferito che il sistema aveva completato una prova il terzo giorno di lavoro.
Una verifica automatica controlla una dimostrazione formulata in modo preciso; il confronto tra quella formulazione e la congettura originale resta un passaggio matematico distinto.
Che cosa afferma la formalizzazione
La congettura riguarda l’influenza delle variabili in un polinomio: in certe condizioni, almeno un bit dell’input deve incidere in misura non trascurabile sul valore del polinomio. Il repository di PSI formalizza un polinomio reale di grado al massimo d, con valori compresi tra 0 e 1 su tutte le stringhe binarie di lunghezza N, e con varianza rispetto agli input uniformi di almeno ε > 0.
L’influenza di una coordinata è la media del cambiamento al quadrato nel valore del polinomio quando si capovolge il bit corrispondente. In notazione del repository, Inf_i[p] = E_X[(p(X) − p(X^i))²]: X^i è la stringa X con il bit i invertito.
Per queste condizioni, il repository riporta un limite inferiore esplicito, (8√15/(125π⁴)) · ε^(5/2)/d⁶, e indica anche la forma (ε/d)^7 per l’enunciato PrintedConjecture, nella normalizzazione usata da PSI. La formulazione chiarisce così quali ipotesi e quale quantità matematica sono coinvolte; il repository precisa anche che i lettori devono confermare che PrintedConjecture esprima la congettura prevista.
Che cosa controlla Lean
Lean è un assistente di dimostrazione: verifica passaggi matematici espressi in un linguaggio formale. Il repository elenca quattro dichiarazioni finali di teoremi e riferisce che la formalizzazione è stata controllata con il kernel di Lean e riprodotta anche con lean4lean. Secondo il repository, lo sviluppo formale non contiene segnaposto né assiomi aggiunti.
Questi controlli riguardano le proposizioni formalizzate e le dimostrazioni che Lean può verificare. Non decidono da soli se la definizione di PrintedConjecture coincide con il significato della congettura originale; inoltre, il testo matematico leggibile da una persona non è interamente controllato dalla formalizzazione. Il repository include nella base di fiducia anche il kernel e il compilatore di Lean, le definizioni della libreria Mathlib e le macchine che eseguono i controlli.
PSI ha detto il 6 novembre che Guy Blanc, Jordan Docter, Carmen Strassle e Li-Yang Tan, ricercatori di Stanford, stavano leggendo la prova, avevano inviato commenti e preparavano una versione più breve dell’esposizione per gli esperti. La loro attività è distinta dai controlli automatici descritti nel repository.
Che cosa implica per le query quantistiche
PSI collega il risultato alla complessità delle query, cioè al numero di accessi ai dati di input. Secondo la sua spiegazione, la probabilità che un algoritmo quantistico risponda «sì» dopo T query è rappresentabile da un polinomio limitato di grado al massimo 2T.
La conseguenza descritta da PSI riguarda la possibilità di approssimare quella probabilità con un numero polinomiale di letture classiche dell’input per la maggior parte degli input casuali, quando l’errore ammesso e la frazione di input considerata sono fissati. È una conclusione sul numero di query in questo specifico modello; non è un limite generale sul tempo totale di esecuzione di qualsiasi algoritmo quantistico. La spiegazione di PSI circoscrive così l’implicazione della congettura senza estenderla a ogni problema di calcolo quantistico.
