PSI meldt door de machine gecontroleerd bewijs voor het vermoeden van Aaronson en Ambainis

Physical Superintelligence maakte op 6 november 2026 bekend dat een intern onderzoekssysteem, dat instanties van een niet-openbaar model van Anthropic draaide, een bewijs had gevonden voor het vermoeden van Aaronson en Ambainis, een vraagstuk in de kwantumcomputing dat sinds 2008 onopgelost was.

Het systeem leverde op de derde dag van een run op PSI’s eigen infrastructuur een volledig bewijs, dat door de Lean-bewijsassistent werd aanvaard. Vervolgens legde PSI verwante open problemen aan het systeem voor. Dat verbeterde het resultaat tweemaal, voordat Lean de definitieve versie aanvaardde. Het manuscript en de formalisering in Lean 4 zijn openbaar.

Wat het vermoeden zegt over kwantumversnelling

De vraag is wanneer kwantumcomputers exponentieel sneller kunnen zijn dan klassieke computers. Shors factorisatiealgoritme uit 1994 is afhankelijk van structuur: de invoer bevat een herhalend patroon dat het algoritme kan benutten. Het resultaat van PSI gaat over het tegenovergestelde geval, met willekeurige of ongestructureerde invoer, waarin zo’n patroon doorgaans ontbreekt.

In het querymodel leest een klassiek algoritme per query één bit, terwijl een kwantumquery in superpositie over meerdere invoerposities kan worden verdeeld. PSI legt het verband tussen dit model en polynomen: na T kwantumqueries is de kans dat het algoritme ‘ja’ antwoordt een begrensd polynoom van de invoerbits met een graad van hoogstens 2T. Het simuleren van het kwantumalgoritme komt er daarom op neer dat polynoom te schatten zonder exponentieel veel invoerbits te lezen.

In hun oorspronkelijke artikel vermoedden Scott Aaronson en Andris Ambainis dat elk begrensd polynoom van lage graad een zeer invloedrijke variabele heeft. Ze bewezen dat, als het vermoeden klopt, elk kwantumalgoritme met T queries voor de meeste invoeren kan worden gesimuleerd door een klassiek algoritme dat polynomiaal veel queries in T uitvoert. Dat betekent dat het aantal klassieke queries voor elke vaste benaderingsfout en elk vast aandeel uitgesloten invoeren polynomiaal in plaats van exponentieel groeit; het sluit exponentiële kwantumvoordelen bij problemen met een geschikte structuur niet uit.

Formeel beschouwt de repository een reëel polynoom p met een graad van hoogstens d, waarvan de waarden op de discrete kubus tussen 0 en 1 liggen. Als de variantie ervan over een willekeurig gekozen invoer minstens ε is, heeft een bepaalde coördinaat een invloed van minstens (8√15 / (125π⁴)) · ε^(5/2) / d⁶, en daarmee ook minstens (ε/d)⁷. Invloed is de verwachte gekwadrateerde verandering in p wanneer de bitwaarde van die coördinaat wordt omgedraaid.

Hoe het bewijs tot stand kwam en werd gecontroleerd

Het bewijs volgt een plan van Shachar Lovett en Jiapeng Zhang, gebaseerd op fractionele certificaten en niveauverzamelingen, maar vervangt een ongelijkheid die in hun plan slechts werd vermoed door een nieuwe ongelijkheid die voor alle paren geldt. Een determinant levert een één-op-éénkoppeling van invoerinstellingen op. Volgens PSI gaat deze koppeling verder dan de zwakkere koppeling uit David Reimers Butterfly-lemma, omdat ze ook begrenst hoe vaak gekoppelde instellingen op elke coördinaat overeenkomen; die begrenzing is nodig voor de nieuwe ongelijkheid.

De repository verdeelt het elementaire bewijs in vier onderdelen: de ongelijkheid voor alle paren afleiden uit de determinant en de bijectie, die ongelijkheid integreren over niveauverzamelingen, middelen over coördinaten en een rijgrens vaststellen met behulp van een puntsgewijze gevoeligheidsgrens. Samen leveren deze stappen de expliciete invloedsgrens op.

Volgens de vastgelegde controle van de repository bevat de formele uitwerking geen bewijsplaatsaanduidingen of toegevoegde axioma’s. De declaraties zijn opnieuw uitgevoerd via de kernel van Lean en lean4lean, een onafhankelijke implementatie van Lean’s typechecker. In een afgeschermde omgeving aanvaardde een vergelijker die de nanoda- en Lean-kernels gebruikte de vier definitieve stellingen. Op een tweede machine aanvaardde die één correcte kleine oplossing en verwierp hij vier opzettelijk onjuiste oplossingen.

Aan die controles zijn duidelijke beperkingen verbonden. Een lezer moet nog steeds nagaan of de formele stelling overeenkomt met het gepubliceerde vermoeden. Het voor mensen leesbare artikel is zelf niet machinaal gecontroleerd. Bovendien blijven Lean’s kernel en compiler, de definities in Mathlib en de machines waarop de controles zijn uitgevoerd onderdeel van de vertrouwde basis.

De rol van mensen en beoordeling door experts

David Turturean, lid van de technische staf van PSI, ontwikkelde en draaide het onderzoekssysteem, bakende het probleem af, gaf het model de opdracht een eerste versie samen te stellen en beoordeelde die versie. Hij is verantwoordelijk voor de juistheid van het artikel. De repository vermeldt dat AI-modellen de wiskundige beweringen, de eerste versie en de formalisering in Lean hebben opgesteld. Jim Halverson controleerde het bewijs en Phiala Shanahan gaf commentaar op de formalisering.

De aankondiging volgt op een artikel dat op 19 augustus 2026 is ingediend door Guy Blanc, Jordan Docter, Carmen Strassle en Li-Yang Tan. Deze auteurs hadden het gevolg voor klassieke simulatie bij parallelle kwantumalgoritmen al vastgesteld: ze bewezen dat een algoritme met t queries en d rondes voor de meeste invoeren kan worden gesimuleerd met t^(O(d²)) klassieke queries. Volgens PSI hebben ze alle vier het volledige bewijs gelezen en van commentaar voorzien; ook werken ze aan een kortere uiteenzetting voor experts.

In hun beoordeling, gepubliceerd door PSI, schreven de onderzoekers: “Dit is een enorm resultaat. Het lost een vermoeden op dat al tientallen jaren bestaat en belangrijke implicaties heeft voor de aard van problemen die kwantumversnelling toelaten. Het bewijs bouwt voort op en breidt verschillende onderzoekslijnen uit op het gebied van de analyse van booleaanse functies en de probabilistische combinatoriek. Alles wordt op een tamelijk magische manier samengebracht.”

De directe toets is uitzonderlijk concreet: onafhankelijke kernels kunnen het gecodeerde betoog opnieuw uitvoeren, terwijl experts nog moeten bevestigen dat de gecodeerde uitspraak overeenkomt met het vermoeden van Aaronson en Ambainis, en de delen van het artikel beoordelen die buiten Lean vallen. Die taakverdeling bepaalt wat de machinecontroles aantonen en waarvoor nog menselijke wiskundige beoordeling nodig is.