Community
PSI dimostra la congettura di Aaronson-Ambainis
- Un problema aperto dal 2008, tra i centrali della complessità quantistica, diventa teorema: ogni polinomio di basso grado con valori fra 0 e 1 ha almeno una variabile influente. Conseguenza: su domande sì/no con input casuali un computer quantistico è al massimo polinomialmente più veloce di uno classico. Gli speedup esponenziali, come quello di Shor, restano possibili solo quando l'input ha una struttura particolare.
- Il bound è esplicito:
Inf_i ≥ c·ε^(5/2)/d^6 ≥ (ε/d)^7, con c ≈ 0,0025 ed ε la varianza. La prova l'ha trovata un sistema di ricerca interno di PSI basato su un modello Anthropic non pubblico, completa già al terzo giorno di esecuzione; poi il sistema ha migliorato il risultato due volte. Riprende idee di Lovett e Zhang, del Butterfly Lemma di Reimer e di altri lavori. - Tutto è formalizzato in Lean 4, senza placeholder né assiomi aggiunti, e ricontrollato da due implementazioni indipendenti del kernel. Paper e codice sono pubblici. I ricercatori di Stanford che ad agosto avevano risolto un caso particolare (Blanc, Docter, Strassle, Tan) lo definiscono "un risultato enorme", con implicazioni importanti su quali problemi ammettono speedup quantistici.
