PSI informuje o strojově ověřeném důkazu domněnky Aaronsona a Ambainise

Společnost Physical Superintelligence oznámila 6. listopadu 2026, že interní výzkumný systém využívající instance neveřejného modelu Anthropic nalezl důkaz domněnky Aaronsona a Ambainise, problému v oblasti kvantových výpočtů, který zůstával otevřený od roku 2008.

Systém vytvořil úplný důkaz třetí den běhu na vlastní infrastruktuře PSI a dokazovací asistent Lean jej přijal. PSI pak systému zadala související otevřené problémy; systém výsledek dvakrát vylepšil, než Lean přijal konečnou verzi. Rukopis a formalizace v Lean 4 jsou veřejně dostupné.

Co domněnka říká o kvantovém zrychlení

Otázka se týká toho, kdy mohou být kvantové počítače exponenciálně rychlejší než klasické stroje. Shorův faktorizovací algoritmus z roku 1994 závisí na struktuře: jeho vstup obsahuje opakující se vzorec, který může algoritmus využít. Výsledek PSI se zabývá opačným případem náhodných či nestrukturovaných vstupů, u nichž takový vzorec obecně chybí.

V modelu dotazů klasický algoritmus při každém dotazu přečte jeden bit, zatímco kvantový dotaz může být v superpozici rozprostřen mezi mnoha pozicemi vstupu. PSI tento model vysvětluje pomocí polynomů: po T kvantových dotazech je pravděpodobnost, že algoritmus odpoví kladně, omezeným polynomem vstupních bitů stupně nejvýše 2T. Simulace kvantového algoritmu se proto mění v otázku, jak tento polynom odhadnout, aniž bychom přečetli exponenciálně mnoho vstupních bitů.

Ve své původní práci vyslovili Scott Aaronson a Andris Ambainis domněnku, že každý omezený polynom nízkého stupně má proměnnou s velkým vlivem. Dokázali, že za předpokladu platnosti této domněnky lze každý kvantový algoritmus s T dotazy simulovat na většině vstupů klasickým algoritmem, který provede polynomiálně mnoho dotazů vzhledem k T. Důsledkem je polynomiální, nikoli exponenciální růst počtu klasických dotazů při libovolné pevně dané chybě aproximace a podílu vynechaných vstupů; nevylučuje to exponenciální výhodu kvantových počítačů u problémů s vhodnou strukturou.

Formálně se v repozitáři uvažuje reálný polynom p stupně nejvýše d, jehož hodnoty na diskrétní krychli leží mezi 0 a 1. Pokud je jeho rozptyl při rovnoměrně náhodném vstupu alespoň ε, má některá souřadnice vliv alespoň (8√15 / (125π⁴)) · ε^(5/2) / d⁶, a tedy alespoň (ε/d)⁷. Vliv je očekávaná druhá mocnina změny p při převrácení bitu dané souřadnice.

Jak byl důkaz sestaven a ověřen

Důkaz vychází z plánu Shachara Lovetta a Jiapenga Zhanga založeného na frakčních certifikátech a hladinových množinách, jednu nerovnost, kterou tento plán ponechal jako domněnku, však nahrazuje novou nerovností pro všechny dvojice. Determinant vytváří bijektivní párování nastavení vstupu. Podle PSI toto párování překonává slabší párování z Reimerova motýlího lemmatu, protože také omezuje, jak často se spárovaná nastavení shodují v jednotlivých souřadnicích. Tato mez je pro novou nerovnost nezbytná.

Repozitář rozděluje elementární důkaz do čtyř částí: odvození nerovnosti pro všechny dvojice z determinantu a bijekce, její integraci přes hladinové množiny, zprůměrování přes souřadnice a stanovení meze pro řádky pomocí bodové meze citlivosti. Tyto kroky společně vedou k explicitní mezi vlivu.

Podle zaznamenaného auditu v repozitáři formální vývoj neobsahuje žádné zástupné důkazy ani dodatečné axiomy. Jeho deklarace byly znovu ověřeny prostřednictvím jádra Lean a nástroje lean4lean, nezávislé implementace typového kontroloru Lean. V izolovaném běhu přijal kontrolní program využívající jádra nanoda a Lean všechny čtyři konečné věty; na druhém stroji přijal jedno správné malé řešení a odmítl čtyři záměrně chybné.

Tato ověření mají jasně vymezené limity. Čtenář musí stále potvrdit, že formální tvrzení odpovídá zveřejněnému znění domněnky. Článek v podobě určené ke čtení není sám o sobě strojově ověřen a součástí důvěryhodného základu zůstávají jádro a překladač Lean, definice Mathlibu i stroje použité k ověřování.

Role lidí a odborné posouzení

David Turturean, člen technického týmu PSI, vytvořil a provozoval výzkumný systém, vymezil problém, navedl model, aby připravil první návrh, tento návrh zkontroloval a odpovídá za správnost článku. Repozitář uvádí, že matematická tvrzení, první návrh i formalizaci v Lean vytvořily modely umělé inteligence. Jim Halverson provedl audit důkazu a Phiala Shanahan se vyjádřila k formalizaci.

Oznámení navazuje na článek odevzdaný 19. srpna 2026, jehož autory jsou Guy Blanc, Jordan Docter, Carmen Strassle a Li-Yang Tan. Tito autoři vyřešili důsledek pro klasickou simulaci paralelních kvantových algoritmů a dokázali, že algoritmus s t dotazy a d koly lze simulovat na většině vstupů pomocí t^(O(d²)) klasických dotazů. PSI uvádí, že všichni čtyři studují celý důkaz, poskytli k němu připomínky a připravují kratší výklad pro odborníky.

Ve svém hodnocení zveřejněném organizací PSI vědci napsali: „Jde o obrovský výsledek. Vyřešuje domněnku starou desítky let, která má důležité důsledky pro povahu problémů umožňujících kvantové zrychlení. Důkaz čerpá z několika směrů výzkumu analýzy Booleových funkcí a pravděpodobnostní kombinatoriky a dále je rozvíjí. Všechno je propojeno poměrně magickým způsobem.“

Bezprostřední ověření je neobvykle konkrétní: nezávislá jádra mohou znovu ověřit zakódovaný argument, odborníci však stále musí potvrdit, že zakódované tvrzení odpovídá domněnce Aaronsona a Ambainise, a posoudit části článku, které nejsou v systému Lean. Toto rozdělení určuje, co kontroly provedené strojem potvrzují a co ještě vyžaduje lidské matematické posouzení.