Op 6 november 2026 zei Physical Superintelligence (PSI) dat een intern systeem, dat gebruikmaakte van een niet-openbaar model van Anthropic, een bewijs van het vermoeden van Aaronson–Ambainis had geproduceerd dat Lean accepteerde. PSI’s openbare repository beschrijft precies welke wiskundige uitspraak is geformaliseerd. Het laat aan lezers over om te beoordelen of die uitspraak overeenkomt met het bedoelde vermoeden. PSI’s aankondiging en de openbare Lean-repository leggen elk een ander deel van de claim vast.
Wat de formele stelling zegt
Het vermoeden gaat over de invloed van afzonderlijke bits op een begrensd polynoom. De repository formaliseert een reëel polynoom met graad hoogstens d, waarvan de waarden tussen 0 en 1 liggen voor alle binaire invoeren in {0,1}^N. De variantie onder een uniforme verdeling over die invoeren moet minstens ε zijn.
Voor zo’n polynoom stelt de repository dat er minstens één bit is waarvan de invloed een ondergrens haalt van (8√15/(125π⁴))·ε^(5/2)/d⁶; de repository vermeldt daarnaast de ondergrens (ε/d)^7. Invloed betekent hier de verwachte gekwadrateerde verandering in de waarde van het polynoom wanneer je één bit omklapt. De uitspraak zegt dus dat ten minste één invoervariabele ertoe doet, onder de genoemde voorwaarden. De repository specificeert de formele stelling en de invloedmaat.
De Lean-formalisering bevat een stelling met de naam aaronson_ambainis. De repository noemt de propositie PrintedConjecture de conjectuur in PSI’s normalisatie, met de grens (ε/d)^7. Die naam en de machinecontrole maken de semantische stap niet automatisch: de repository zegt dat lezers zelf moeten nagaan of de formele uitspraak het bedoelde vermoeden weergeeft.
Lean kan controleren of een formeel bewijs uit de vastgelegde definities volgt. De betekenis van die definities ten opzichte van het oorspronkelijke vermoeden vraagt ook om menselijke beoordeling.
Wat Lean controleert
Lean is een bewijsassistent: een systeem dat formele bewijzen controleert volgens vastgelegde regels. PSI zegt dat het systeem tijdens de derde dag van zijn run een volledig bewijs had en dat Lean de formalisering accepteerde. De repository vermeldt vier definitieve Lean-stellingen en zegt dat de formele ontwikkeling geen placeholders of extra axioma’s bevat. Ook meldt de repository dat de stellingen opnieuw zijn gecontroleerd met Lean’s kernel en lean4lean.
Die controles gaan over de formele uitspraken en bewijzen. De repository zegt dat ze niet vaststellen of PrintedConjecture het bedoelde vermoeden weergeeft. Ook de leesbare wiskundige paper is niet volledig door de machine gecontroleerd. De repository rekent Lean’s kernel en compiler, de definities in Mathlib en de controlecomputers tot de basis waarop de controle vertrouwt.
Wat PSI zegt over quantumqueries
De relevantie voor quantumcomputers ligt hier in de querycomplexiteit: het aantal keren dat een algoritme informatie over zijn invoer mag opvragen. Volgens PSI is de kans dat een quantumalgoritme na T queries ‘ja’ antwoordt, weer te geven als een begrensd polynoom met graad hoogstens 2T.
PSI verbindt het vermoeden aan een beperktere consequentie: voor een vaste foutmarge en een vaste fractie invoeren kan een klassiek algoritme met polynomiaal veel invoerlezingen de ja-kans benaderen voor alle invoeren behalve een klein deel van willekeurige invoeren. Dat gaat over queryaantallen in dit model; PSI beschrijft daarmee geen algemene grens voor de totale uitvoeringstijd van willekeurige quantumtaken. PSI licht die gevolgtrekking toe bij de aankondiging.
PSI meldde op 6 november dat Guy Blanc, Jordan Docter, Carmen Strassle en Li-Yang Tan van Stanford de proof lazen, opmerkingen hadden gestuurd en werkten aan een kortere uiteenzetting voor experts.
