OpenAI claimt AI-bewijzen voor ETH, Kakeya en Yang-Mills

OpenAI heeft maandag 26 oktober drie onderzoeksresultaten gepresenteerd die volgens het bedrijf door een intern AI-model zijn gevonden. Het gaat om een weerlegging van de Exponential Time Hypothesis (ETH) uit de informatica, een bewijs van het local smoothing-vermoeden uit de wiskunde en een bewijs dat bepaalde kwantumveldentheorieën wiskundig bestaan. Geen van de drie is al door vakgenoten beoordeeld, meldt The Next Web.

Wat OpenAI precies claimt

De ETH is een vermoeden over hoe moeilijk het satisfiability-probleem (SAT) is. Het hangt nauw samen met de vraag P versus NP, en talloze hardheidsresultaten in graftheorie, computationele biologie en databases leunen erop. In zijn blogpost noemt OpenAI de hypothese zelf “widely believed to be true”. Het model vond de weerlegging op 16 oktober. Een dag later was het bewijs gecontroleerd in Lean, een programmeertaal waarin een computer elke stap van een bewijs naloopt. De uitwerking en de Lean-code staan op GitHub.

Het geclaimde algoritme voor 3-SAT is sneller dan exponentieel, maar niet polynomiaal. P = NP volgt er dus niet uit. OpenAI schrijft zelf dat bruikbare algoritmes nog “significant further research” vragen.

Het tweede resultaat is een bewijs van het local smoothing-vermoeden, in 1991 geformuleerd door Christopher Sogge, in alle dimensies. Volgens OpenAI volgen daaruit ook het Kakeya-vermoeden en het restrictievermoeden van Stein in alle dimensies. Tot nu toe was local smoothing alleen in twee dimensies bewezen (2019) en Kakeya in drie (2025). Het derde resultaat komt uit de natuurkunde: een rigoureus bewijs dat bepaalde vierdimensionale kwantumveldentheorieën bestaan, waaronder kwantumchromodynamica. Daarin zit ook het bestaan van zuivere Yang-Mills-theorie, een onderdeel van een van de Millenniumproblemen van het Clay Institute.

Wie het gaat controleren

Voor de ETH-claim leiden Russell Impagliazzo en Ramamohan Paturi (UC San Diego) en Ryan Williams (MIT) een onafhankelijke toetsing. Impagliazzo en Paturi stelden de hypothese ooit zelf op, samen met Francis Zane. In een open brief schrijven ze dat hun betrokkenheid geen steunbetuiging is. Ze tekenden geen geheimhoudingsverklaring en worden niet betaald.

Het drietal stelde twee voorwaarden: OpenAI moet alle ruwe data achter het resultaat vrijgeven en een conferentie voor de onderzoeksgemeenschap betalen. Volgens Williams en OpenAI is het bedrijf met beide akkoord gegaan. Het natuurkundewerk ligt bij een groep rond Nobelprijswinnaar David Gross, met onder anderen Arthur Jaffe en Nikita Nekrasov. Zij geven het AI-materiaal voorlopig niet vrij en schrijven het werk zelf uit, waardoor buitenstaanders het nu nog niet kunnen controleren.

De vraag wie de eer krijgt

OpenAI zegt geen academische erkenning te zoeken. Die moet naar de onderzoekers gaan die de resultaten uitleggen. Het bedrijf gaf 5 miljoen dollar aan de Simons Foundation voor workshops en conferenties over door AI geproduceerde resultaten. De drie ETH-onderzoekers zijn sceptischer. Zij waarschuwen dat de eer straks gaat naar wie het eerst publiceert of de krachtigste rekenkracht heeft, terwijl het controlewerk weinig oplevert. Dezelfde zorg stond in de verklaring die wiskundigen in juni in Leiden opstelden.

Wat betekent dit

De claims passen in een reeks. Begin oktober publiceerde OpenAI 722 wiskundepapers van een intern model, en vorige week bewezen Microsoft-onderzoekers het KLS-vermoeden met hulp van AI. Ook Anthropic laat Claude steeds vaker formele bewijzen leveren en rekenwerk in de natuurkunde doen.

Het verschil is de schaal. Klopt de ETH-weerlegging, dan moeten leerboeken over complexiteitstheorie worden herschreven. Een Lean-bewijs maakt fouten in de redenering onwaarschijnlijk, maar zegt niets over de vraag of de formalisering precies het juiste vermoeden vastlegt. Daarvoor zijn mensen nodig, en dat kost maanden. Tot die toetsing klaar is, blijven het claims van één bedrijf, hoe goed onderbouwd ze ook lijken.