PSI rapporterar om maskinkontrollerat bevis för Aaronson–Ambainis-förmodan

Physical Superintelligence meddelade den 6 november 2026 att ett internt forskningssystem som körde instanser av en icke-offentlig modell från Anthropic hade hittat ett bevis för Aaronson–Ambainis-förmodan, ett problem inom kvantberäkning som varit olöst sedan 2008.

Systemet producerade ett fullständigt bevis under den tredje dagen av en körning på PSI:s egen infrastruktur, och Lean-bevisassistenten godtog det. PSI gav därefter systemet närliggande öppna problem att lösa, och systemet förbättrade resultatet två gånger innan Lean godtog den slutliga versionen. Manuskriptet och formaliseringen i Lean 4 är offentliga.

Vad förmodan säger om kvantförsprång

Frågan gäller när kvantdatorer kan vara exponentiellt snabbare än klassiska datorer. Shors faktoriseringsalgoritm från 1994 bygger på struktur: dess indata innehåller ett upprepande mönster som algoritmen kan utnyttja. PSI:s resultat behandlar det motsatta fallet, med slumpmässiga eller ostrukturerade indata, där ett sådant mönster i allmänhet saknas.

I frågemodellen läser en klassisk algoritm en bit per fråga, medan en kvantfråga kan fördelas i en superposition över många positioner i indatan. PSI:s förklaring kopplar modellen till polynom: efter T kvantfrågor är sannolikheten att algoritmen svarar ja ett begränsat polynom av indatabitarna med grad högst 2T. Att simulera kvantalgoritmen blir därför en fråga om att uppskatta polynomet utan att läsa exponentiellt många indatabitar.

I sin ursprungliga artikel förmodade Scott Aaronson och Andris Ambainis att varje begränsat polynom av låg grad har en variabel med stort inflytande. De visade att varje kvantalgoritm med T frågor, under antagandet att förmodan stämmer, kan simuleras på de flesta indata av en klassisk algoritm som gör polynomiskt många frågor i T. Följden är en polynomisk snarare än exponentiell ökning av antalet klassiska frågor, för varje fast approximationsfel och andel uteslutna indata; resultatet utesluter inte exponentiella kvantfördelar för problem med lämplig struktur.

Formellt betraktar arkivet ett reellt polynom p av grad högst d, vars värden på den diskreta kuben ligger mellan 0 och 1. Om dess varians över en likformigt slumpmässig indata är minst ε, har någon koordinat ett inflytande på minst (8√15 / (125π⁴)) · ε^(5/2) / d⁶ och därmed minst (ε/d)⁷. Inflytande är den förväntade kvadrerade förändringen i p när biten för den koordinaten byter värde.

Så byggdes och kontrollerades beviset

Resonemanget följer en plan av Shachar Lovett och Jiapeng Zhang, som bygger på fraktionella certifikat och nivåmängder, men ersätter en olikhet som planen lämnade som en förmodan med en ny olikhet som gäller för alla par. En determinant skapar en ett-till-ett-parning av indatavärden. PSI uppger att denna parning går längre än David Reimers svagare parning i Butterfly Lemma, eftersom den också begränsar hur ofta parade värden överensstämmer i varje koordinat, en gräns som behövs för den nya olikheten.

Arkivet delar upp det elementära beviset i fyra delar: att härleda olikheten för alla par från determinanten och bijektionen, integrera den över nivåmängder, ta medelvärdet över koordinater och fastställa en radsgräns med hjälp av en punktvis känslighetsgräns. Tillsammans ger dessa steg den explicita gränsen för inflytandet.

Enligt arkivets dokumenterade granskning innehåller den formella utvecklingen inga platshållare för bevis eller tillagda axiom. Deklarationerna kördes på nytt genom Leans kärna och lean4lean, en oberoende implementation av Leans typkontroll. I en sandlådemiljö godtog en jämförare som använde nanoda- och Lean-kärnorna de fyra slutliga satserna. På en andra dator godtog den en korrekt, liten lösning och avvisade fyra avsiktligt felaktiga lösningar.

Kontrollerna har uttryckliga begränsningar. Läsaren måste fortfarande bekräfta att den formella formuleringen motsvarar den publicerade förmodan. Den text som är avsedd för människor är inte i sig maskinkontrollerad, och Leans kärna och kompilator, Mathlibs definitioner samt datorerna som användes för kontrollerna ingår fortfarande i den betrodda basen.

Människornas roller och expertgranskning

David Turturean, medlem av PSI:s tekniska personal, utvecklade och körde forskningssystemet, avgränsade problemet, bad modellen sammanställa ett första utkast, granskade utkastet och ansvarar för artikelns korrekthet. Arkivet upplyser om att AI-modeller producerade de matematiska påståendena, det första utkastet och Lean-formaliseringen. Jim Halverson granskade beviset och Phiala Shanahan lämnade synpunkter på formaliseringen.

Meddelandet kommer efter en artikel som lämnades in den 19 augusti 2026 av Guy Blanc, Jordan Docter, Carmen Strassle och Li-Yang Tan. Dessa författare hade fastställt följden för klassisk simulering av parallella kvantalgoritmer och bevisat att en algoritm med t frågor och d omgångar kan simuleras på de flesta indata med t^(O(d²)) klassiska frågor. PSI uppger att alla fyra har läst hela beviset, lämnat synpunkter och förbereder en kortare framställning för experter.

I sin bedömning, som publicerades av PSI, skrev forskarna: ”Det här är ett mycket betydelsefullt resultat. Det löser en decenniegammal förmodan med viktiga implikationer för vilka problem som kan ge kvantumfördelar. Beviset bygger på och vidareutvecklar flera forskningslinjer inom analys av booleska funktioner och probabilistisk kombinatorik. Allt sammanförs på ett närmast magiskt sätt.”

Det omedelbara testet är ovanligt konkret: oberoende kärnor kan återskapa det kodade argumentet, medan experter fortfarande måste bekräfta att det kodade påståendet stämmer överens med Aaronson och Ambainis konjektur och bedöma de delar av artikeln som ligger utanför Lean. Denna uppdelning avgör vad maskinkontrollerna fastställer och vad som fortfarande kräver mänsklig matematisk granskning.