OpenAI geeft drie AI-claims elk een andere toetsingsroute

OpenAI meldt op 26 oktober drie nieuwe onderzoeksclaims in wiskunde, informatica en natuurkunde en koppelt elk vakgebied aan een andere route voor academische begeleiding.

Voor Nederlandse R&D-teams die leveranciersclaims beoordelen, verandert vooral de bewijsroute: de ETH-claim staat in een openbaar Lean-bestand, maar vakgenoten moeten de formele stelling nog toetsen aan de bedoelde wiskundige claim. Bij het natuurkundeonderzoek houdt OpenAI de AI-uitvoer voorlopig achter. Het gaat om intern modelonderzoek, niet om een nieuw bedrijfsproduct.

De ETH-claim staat als formele stelling in Lean

De informaticaclaim raakt de Exponential Time Hypothesis (ETH), een aanname achter honderden resultaten over de moeilijkheid van problemen in onder meer grafentheorie en databases. OpenAI zegt dat zijn model ETH weerlegt. Als dat standhoudt, verandert welke theoretische grenzen onderzoekers voor zulke problemen aannemen. OpenAI schrijft dat nog veel werk nodig is om de resultaten in betere algoritmen en praktische winst om te zetten.

Het model maakte op 16 oktober een tekstueel bewijs; een dag later werd dat in Lean geformaliseerd. De openbare Lean-stelling betreft een algoritme dat voor vaste k vanaf 2 het exacte aantal toekenningen berekent die canoniek gecodeerde k-CNF-formules waar maken in subexponentiële tijd en polynomiale ruimte. Dit is de formele uitspraak die ETH tegenspreekt, geen claim dat elk praktisch SAT-probleem nu snel oplosbaar is.

Lean controleert of het bewijs volgt uit de formele stelling, definities en axioma’s. De taalreferentie waarschuwt dat ook moet kloppen dat de formele stelling overeenkomt met de bedoelde betekenis in gewone wiskundetaal. Die aansluiting wordt dus nog door mensen beoordeeld. De groep wordt geleid door Russell Impagliazzo en Ramamohan Paturi van UC San Diego en Ryan Williams van MIT; Impagliazzo en Paturi waren mede-indieners van ETH. OpenAI vroeg hen het bewijs te onderzoeken en de redenering publiekelijk uit te leggen. De drie benadrukken dat hun betrokkenheid geen certificering is. Zij vragen toegang tot alle ruwe data; OpenAI zegt die te delen en een conferentie te financieren.

Wiskunde en natuurkunde volgen andere routes

De wiskundige claim betreft de lokale afvlakkingsvermoedens voor golven, voorgesteld door Christopher Sogge in 1991. OpenAI zegt dat het model een bewijs voor alle dimensies vond, dat ook de Kakeya- en Stein-vermoedens in alle dimensies zou oplossen. Eerdere resultaten betroffen twee dimensies voor lokale afvlakking in 2019 en drie dimensies voor Kakeya in 2025. Het resultaat verscheen op 18 oktober en kreeg op 19 oktober een Lean-formalisering; beide bestanden zijn openbaar. OpenAI moedigt onderzoekers aan zelf groepen te vormen om de uitwerking toe te lichten.

In de natuurkunde claimt OpenAI een rigoureus bestaansbewijs voor bepaalde vierdimensionale quantumveldtheorieën, waaronder kwantumchromodynamica (QCD) en een voltooiing van het Standaardmodel. Ook noemt het pure Yang-Mills, onderdeel van een Millenniumprobleem van het Clay Mathematics Institute. Het model produceerde de Yang-Mills-uitkomst op 9 september en QCD op 18 september. Alleen de Yang-Mills-formalisering was op 16 oktober klaar. De natuurkundegroep rond David Gross houdt de AI-uitvoer achter en schrijft zelf een uitleg; OpenAI zegt niet dat QCD al in Lean staat.

De eerdere vrijgaven krijgen versiegeschiedenis

OpenAI meldde in september dat een intern model ruim honderd open wiskundeproblemen had opgelost en stelde een adviesgroep in. Op 6 oktober publiceerde het 722 manuscripten in 372 resultaatfamilies. De repository telt nu 721 manuscripten in 373 families; circa 42 procent van de hoofdresultaten heeft een Lean-formalisering. OpenAI waarschuwt dat ongeformaliseerde resultaten problemen kunnen bevatten.

De versiegeschiedenis laat zien waarom dat voorbehoud telt: op 7 oktober trok OpenAI drie manuscripten in en herzag het er veertien; op 26 oktober kwamen twee Lean-geformaliseerde manuscripten bij. Oudere versies blijven beschikbaar. The Verge plaatst de begeleiding minder dan een maand na de grote vrijgave: twee resultaten krijgen externe begeleiders, terwijl de wiskundige uitvoer direct openbaar is.

Meta koos eerder deze maand voor een andere volgorde: zes papers met Muse Spark kwamen voort uit vragen en redeneringen van wiskundigen. Een tweede groep beoordeelde ze en de papers markeerden welke passages door mensen of AI waren opgesteld. OpenAI start bij intern gemaakte claims en organiseert daarna per discipline uitleg en controle.

De academische gemeenschap kiest niet één route

OpenAI zegt dat de uitgenodigde groepen vrijwillig en onbetaald werken, geen geheimhouding tekenen en onafhankelijk concluderen. Het bedrijf vraagt geen academische erkenning voor de ontdekkingen. Tegelijk erkent OpenAI dat vroege begeleiders selecteren een informatievoorsprong schept.

De onafhankelijke wiskunde-adviesgroep AGMAI adviseerde op 25 oktober tegen het aanwijzen van specifieke wiskundigen voor AI-uitkomsten. De groep noemt ongelijke vroege toegang, ondoorzichtige selectie en het risico dat expert-namen als aanbeveling worden gelezen. Een dag later vroeg AGMAI om de AI- en Lean-uitvoer over Yang-Mills, QCD en het Standaardmodel direct vrij te geven, omdat OpenAI meldde dat de Yang-Mills-formalisering klaar was. Dat staat tegenover de keuze van de natuurkundegroep om de uitvoer voorlopig achter te houden. AGMAI zegt dat het advies niet automatisch op andere wetenschappen slaat en spreekt niet namens alle wiskundigen.

Voor Nederlandse R&D-teams zijn de openbare Lean-bestanden controleerbare formele claims, geen vervanging voor toetsing aan vakliteratuur en uitleg door experts. De ETH-groep moet die beoordeling nog uitvoeren; voor de natuurkunde is de AI-uitvoer niet openbaar en noemt OpenAI geen publicatiedatum. Dat onderscheid bepaalt welke onderbouwing een organisatie vandaag zelfstandig kan inspecteren.