OpenAI publiceert 722 wiskundige manuscripten via AI-model

TL;DR

• Wat: OpenAI heeft 722 wiskundige manuscripten gepubliceerd die zijn gegenereerd door een intern AI-model, waarvan 162 met computerverifieerbare bewijzen.
• Waarom relevant: als AI wiskundige problemen kan oplossen waar mensen decennia over doen, verandert dat op termijn ook wat AI voor bedrijfsprocessen kan betekenen.
• Wat je ermee kunt: volg hoe AI-redeneermodellen zich ontwikkelen — de stap van wiskunde naar complexe bedrijfsvraagstukken is kleiner dan je denkt.

Op 6 oktober maakte OpenAI iets bekend dat in de wiskundewereld flinke opschudding veroorzaakt. Het bedrijf publiceerde 722 wiskundige manuscripten, gemaakt door een intern AI-model dat nog niet publiek beschikbaar is. Ik vind dit interessant omdat het laat zien hoe ver AI-redeneren inmiddels reikt — en wat dat op termijn kan betekenen buiten de wiskunde.

Wat heeft OpenAI precies gepubliceerd?

OpenAI zette een verzameling van 722 manuscripten op GitHub, gegroepeerd in 372 zogenoemde 'resultatenfamilies' verspreid over 17 wiskundige vakgebieden. Denk aan getaltheorie, complexiteitstheorie, meetkunde en wiskundige fysica. Het model dat dit werk heeft geproduceerd, wordt omschreven als een "intern frontier-model" dat krachtiger zou zijn dan GPT-6 Astra — maar de naam is niet bekendgemaakt.

Wat mij hier opvalt, is de schaal. Het model kreeg zo'n 4.000 problemen voorgelegd. De 722 manuscripten zijn het deel dat OpenAI de moeite waard vond om te publiceren. Elk resultaat kostte gemiddeld drie uur rekentijd.

Van die 722 manuscripten zijn er 162 voorzien van een zogenoemde Lean-formalisering. Lean is een programmeertaal waarmee je wiskundige bewijzen kunt omzetten in code, zodat een computer stap voor stap kan controleren of de redenering klopt. Vergelijk het met een boekhoudprogramma dat elke boeking automatisch checkt — als er een logische fout in zit, slaat het alarm.

Dat betekent ook: 560 manuscripten zijn nog níet machinaal geverifieerd. OpenAI waarschuwt daar zelf voor: "Some of the unformalized results could have issues."

Welke resultaten springen eruit?

Een paar van de geverifieerde resultaten zijn opmerkelijk voor wiskundigen:

• Een bewijs over de nulvrije halfvlak voor Dirichlet L-functies bij Re(s) > 7/8 — gerelateerd aan de Riemann-hypothese, maar nadrukkelijk niet hetzelfde. De echte Riemann-hypothese gaat over Re(s) > 1/2 en is nog altijd onopgelost.
• Een bewijs van de symmetrische Mahler-vermoeden.
• Een tegenvoorbeeld voor Kaplansky's nuldeler-vermoeden.

Ik zal eerlijk zijn: ik ben geen wiskundige, dus ik kan de inhoudelijke waarde van deze resultaten niet zelf beoordelen. Maar wat ik wél kan vaststellen is dat wiskundigen als Thomas Bloom van de Universiteit van Manchester dit als "big news" bestempelen.

De Navier-Stokes-controverse

Deze publicatie volgt op een eerdere aankondiging van OpenAI op 8 september, toen het bedrijf claimde dat hetzelfde interne model een bewijs had geleverd rond de Navier-Stokes-vergelijkingen — één van de zeven Millennium Prize Problems, elk goed voor een miljoen dollar. Dat bewijs zou zijn geproduceerd door zo'n 10.000 parallelle AI-agents in 88 uur.

Belangrijke nuance: het gaat niet om het klassieke Millennium-probleem in zijn oorspronkelijke vorm. Het bewijs betreft het ontstaan van een singulariteit onder een 'smooth forcing term' — de versie zonder externe krachten, waar de Clay-prijs aan gekoppeld is, blijft onopgelost.

Bovendien is er een serieuze controverse. De wiskundigen Tristan Buckmaster (NYU) en Levent Alpöge beschuldigden OpenAI ervan dat het model mogelijk gebruik heeft gemaakt van privéchatgesprekken en niet-gepubliceerde concepten die via Codex waren opgeslagen. Dat roept vragen op over data-privacy en wetenschappelijke prioriteit. OpenAI heeft de Millennium-prijs niet geclaimd.

Wat betekent dit voor ondernemers?

Je zou kunnen denken: wiskundige bewijzen, wat heb ik daar als ondernemer aan? Dat is een terechte vraag. Maar wat mij hier fascineert is niet de wiskunde zelf, maar wat het zegt over de redeneercapaciteiten van AI-modellen.

Stel dat je als ondernemer een complex logistiek probleem hebt — voorraadbeheer over meerdere locaties, met seizoenspatronen, levertijden en prijsfluctuaties. Of stel dat je een financieel model wilt bouwen dat rekening houdt met tientallen variabelen tegelijk. De AI-modellen die nu wiskundige bewijzen produceren, gebruiken dezelfde onderliggende capaciteit: langdurig, stapsgewijs redeneren over complexe problemen.

Dat wil niet zeggen dat je morgen een AI-wiskundige op je boekhouding kunt zetten. Maar het laat wel zien in welke richting de technologie beweegt. De stap van "formeel wiskundig bewijs produceren" naar "complexe bedrijfsanalyse uitvoeren" is conceptueel minder groot dan je misschien denkt.

Waar zit de nuance?

Ik vind het belangrijk om hier ook de kanttekeningen te benoemen, want die zijn er.

Ten eerste: het model is niet openbaar. Niemand buiten OpenAI kan het testen, en de resultaten zijn dus lastig onafhankelijk te reproduceren. Dat is een beperking.

Ten tweede: twee wiskundigen merkten op dat zij hun eigen argumenten terugzagen in de gepubliceerde manuscripten. De Lean-verificatie controleert of stap B logisch volgt uit stap A — maar niet of dat argument al eerder door iemand anders is bedacht. Dat is een wezenlijk verschil.

Ten derde: het merendeel van de manuscripten (560 van de 722) mist nog formele verificatie. OpenAI zegt dat er meer formaliseringen komen, maar op dit moment is een groot deel van het werk nog niet machinaal gecontroleerd.

En ten vierde: er is een Advisory Group on Mathematics and Artificial Intelligence opgericht die meer dan 600 reacties uit de wiskundegemeenschap heeft verzameld. Hun aanbeveling is dat resultaten in door wetenschappers beheerde repositories moeten worden gedeponeerd, met transparante documentatie van modelnamen, prompts, rekenkosten en faalpercentages. Dat klinkt als een verstandige eis.

Een observatie om mee af te sluiten

Wat mij het meest bijblijft aan dit verhaal is niet het wiskundige resultaat zelf, maar de spanning tussen mogelijkheid en verificatie. AI kan nu manuscripten produceren die wiskundigen serieus nemen — dat is opmerkelijk. Maar tegelijk is het vertrouwen in die resultaten volledig afhankelijk van onafhankelijke controle, en die loopt achter op de productiecapaciteit.

Voor mij is dat een patroon dat je als ondernemer vaker gaat tegenkomen: AI-systemen die indrukwekkende output leveren, waarbij de vraag verschuift van "kan het dit?" naar "hoe weet ik dat het klopt?" Die tweede vraag wordt de komende jaren wat mij betreft de belangrijkste vraag in elk bedrijf dat serieus met AI aan de slag gaat.