Een maand na de Navier-Stokes-claim komt OpenAI met een stapel van een andere orde. Op 6 oktober zette het bedrijf 722 wiskundige manuscripten op GitHub, allemaal gemaakt door een intern AI-model dat jij en ik niet kunnen gebruiken (Bron: OpenAI). Daartussen zitten claims op problemen waar wiskundigen al decennia op stuklopen. De vraag die het vak nu bezighoudt is niet alleen of het klopt, maar wie dat in vredesnaam gaat nalopen.
Wat er precies op GitHub staat
De repository heet openai/math en bevat 722 manuscripten, verdeeld over 372 families. Een familie is een hoofdresultaat met bijbehorende varianten, gevolgen of alternatieve bewijzen (Bron: OpenAI op GitHub). Alles valt onder de Apache-2.0-licentie, dus iedereen mag het downloaden, controleren en hergebruiken.
Over de werkwijze is OpenAI kort. Het model kreeg tijdens de ontwikkeling ongeveer 4.000 open problemen voorgelegd, en de geslaagde resultaten zijn gebundeld en gefilterd op belang. Elk resultaat kostte gemiddeld zo’n drie uur rekenwerk, uitgedrukt in de denktijd van ChatGPT Pro (Bron: OpenAI op GitHub). OpenAI breidde dit soort tests naar eigen zeggen uit omdat zijn modellen de bestaande wiskunde-benchmarks inmiddels “verzadigd” hadden: die waren te makkelijk geworden.
Een paar titels uit de inhoudsopgave laten zien waar het over gaat (Bron: OpenAI, CONTENTS.md):
| Familie | Wat OpenAI claimt | Lean-bewijs? |
|---|---|---|
| 003 | De quasi-Riemannhypothese: de zetafunctie heeft geen nulpunten rechts van Re(s) = 7/8 | Ja |
| 005 | De constante van Catalan is irrationeel | Ja |
| 017 | De irrationaliteitsexponent van π is precies 2 | Ja |
| 012 | Een vermoeden van Erdős en Pomerance over grootste priemfactoren | Ja |
Voor wie geen wiskundige is: dit zijn geen schoolsommen. De irrationaliteit van de constante van Catalan staat al heel lang open, en de zetafunctie is het hart van de beroemde Riemannhypothese, ook een van de millenniumproblemen. Twee resultaten vielen buiten de vaste procedure: het werk aan de zetafunctie en een bewijs van het Hodge-vermoeden voor een speciale klasse van zogeheten abelse variëteiten. Bij de zetafunctie is één versie van de tekst door mensen herschreven voor de leesbaarheid (Bron: OpenAI op GitHub).
Beginner-tip “irrationeel” betekent dat een getal niet als breuk te schrijven is, zoals π of de wortel uit 2. Bewijzen dat een specifiek getal irrationeel is, blijkt vaak verrassend moeilijk.
Lean: de computer als controleur
Het belangrijkste verschil met een gewone persaankondiging is Lean. Dat is een programmeertaal waarin je een bewijs zo precies opschrijft dat een computer elke logische stap kan controleren. Een Lean-bewijs kan niet overtuigend klinken zonder te kloppen: het slaagt of het faalt (Bron: OpenAI).
Niet alles is zo gecontroleerd. In de inhoudsopgave van 7 oktober telden wij bij ongeveer 235 van de 372 families een link naar een Lean-formalisering, grofweg twee derde. OpenAI schrijft er zelf bij dat “sommige niet-geformaliseerde resultaten problemen kunnen hebben” en belooft fouten snel te herstellen, met een zichtbare versiegeschiedenis (Bron: OpenAI op GitHub).
Gevorderden Een geslaagde Lean-check garandeert dat het statement zoals het in Lean is ingevoerd klopt. Of dat formele statement precies de vraag is die wiskundigen bedoelen, blijft mensenwerk. Bij de Navier-Stokes-claim ging de discussie daar ook over.
Waarom het vak niet staat te juichen
De kritiek is ouder dan deze release. Op 11 september publiceerden Fields-medaillewinnaars, onder wie Terence Tao, Peter Scholze en Maryna Viazovska, de verklaring A Severe Misalignment of AI in Mathematics. De kern:
“The push by AI companies to solve mathematical problems as a benchmark is detrimental to the science of mathematics.” — Verklaring A Severe Misalignment of AI in Mathematics, 11 september 2026 (Bron: mathandai.org)
Hun punt: een beroemd probleem oplossen is in de wiskunde een middel om begrip en nieuwe methoden te krijgen, geen doel op zich (Bron: mathandai.org). Een bewijs dat niemand begrijpt, levert het vak weinig op.
OpenAI reageerde op 21 september met een onafhankelijke adviesgroep bij het Institute for Advanced Study in Princeton, kortweg AGMAI. Er zitten negen wiskundigen in, onder wie Timothy Gowers, Edward Witten en Martin Hairer. Ze worden niet betaald en mogen OpenAI publiekelijk tegenspreken (Bron: OpenAI). Hairer staat overigens ook onder de verklaring van de Fields-medaillewinnaars.
Die adviesgroep was op 29 september niet mals. AI-bedrijven die geavanceerde wiskunde testen op interne modellen kregen te horen: “we do not endorse this practice, and we ask them to stop testing advanced mathematical problems on proprietary models” (Bron: AGMAI). Wie toch publiceert, moet resultaten volgens AGMAI onderbrengen in onafhankelijke wetenschappelijke archieven, prompts, rekentijd en mislukte pogingen openbaar maken, bewijzen formaliseren en het model breed beschikbaar stellen. Anders ontstaat volgens de groep “a two-tier system where labs outrun the rest of the field” (Bron: AGMAI).
Wat OpenAI wel en niet overnam
Leg de release naast dat advies en je ziet een gemengd beeld:
- Wel: formele Lean-bewijzen voor een groot deel, een openbare versiegeschiedenis, samenvattingen van de redenering bij tien resultaten, en de belofte workshops en conferenties te financieren (Bron: OpenAI).
- Niet: het testen op een intern model gaat gewoon door, en het model zelf is niet beschikbaar. De resultaten staan op GitHub, een platform van Microsoft, niet in een onafhankelijk wetenschappelijk archief; OpenAI schrijft dat het “community-hosted” opslag nog onderzoekt (Bron: OpenAI op GitHub).
Het meest opvallende detail zit in de getallen. 722 manuscripten in één keer is meer dan veel wiskundige vakgroepen in jaren produceren. Peer review in de wiskunde is traag omdat een referent een bewijs echt moet doorgronden. Zelfs met Lean als hulpmiddel kost het begrijpen van één serieus resultaat al snel maanden. Daar komt de vraag bij wie de eer krijgt: rond Navier-Stokes ontstond al ruzie met een NYU-wiskundige die zei dat hij er eerder was.
Wat je hier zelf mee doet
Het model ligt niet in de winkel, dus direct merk je er weinig van. Maar het patroon herken je straks overal: een AI-bedrijf meldt een doorbraak, en de echte vraag is wie het buiten dat bedrijf kan narekenen. Drie vragen helpen bij elk volgend bericht:
- Is het bewijs openbaar? Hier wel, en dat is winst ten opzichte van een persbericht.
- Is het machinaal gecontroleerd? Bij grofweg twee derde van de families wel, bij de rest nog niet.
- Hebben onafhankelijke vakmensen het beoordeeld? Nog niet. Dat is precies wat de komende maanden moet blijken.
Hoe zo’n model eigenlijk “nadenkt”, lees je in onze uitleg over redeneermodellen. En waarom een tekst die overtuigend klinkt nog niet hoeft te kloppen, in waarom AI zo zelfverzekerd onzin vertelt. Een eerder voorbeeld van AI in de wetenschap, met een kleiner en beter controleerbaar resultaat, is hoe GPT-5 Pro een raadsel in de immunologie oploste.