In interviews die The Daily Californian op 19 oktober 2026 publiceerde, verschilden UC Berkeley-wiskundigen Richard Borcherds en Robin Huang van mening over AI’s rol in de wiskunde. De technische kritiek op OpenAI’s Navier–Stokesclaim is specifieker: een paper van 6 oktober wijst op verschillen tussen delen van het bewijs in gewone taal en de Lean-formalisering. De auteurs stellen niet dat het geschreven bewijs onjuist is.
Borcherds en Huang verschillen van mening over AI
Borcherds verwacht dat AI binnen enkele jaren menselijke wiskundigen in onderzoek overbodig kan maken. Hij ziet AI-gegenereerde bewijzen niet als een reden om zelf geen wiskunde meer te leren. Huang is sceptischer over de huidige bruikbaarheid van AI voor wiskundig onderzoek en maakt zich zorgen over de gevolgen voor de wiskundegemeenschap. Tegen studenten zei ze dat het gebruik van AI hun eigen beheersing van de stof niet vervangt.
Wat OpenAI over het resultaat zegt
De Navier–Stokesvergelijkingen beschrijven de beweging van vloeistoffen. OpenAI kondigde op 8 september 2026 een resultaat aan over het bestaan en de gladheid van oplossingen voor de driedimensionale vergelijkingen van een onsamendrukbare vloeistof. Volgens het bedrijf laat zijn resultaat zien dat een gladde externe kracht een aanvankelijk gladde vloeistof in rust binnen eindige tijd tot een singulariteit kan brengen, terwijl de energie eindig blijft. OpenAI zegt dat het resultaat de onderdelen C en D van de Clay-formulering behandelt.
NeoTeo schreef eerder over de publicatie van wiskundige resultaten uit een intern AI-model van OpenAI.
Een concreet verschil tussen de tekst en Lean
A. Bastounis, F. Circelli en A. C. Hansen vergelijken in hun paper over de Lean-formalisering onder meer een schatting in Lemma 8.6 met de bijbehorende Lean-schatting. In de versie in gewone taal gaat het om een grens die vier extra afgeleiden vereist; de aangehaalde Lean-schatting vereist er vijf.
| Versie van de schatting | Extra afgeleiden in de betrokken schatting |
| Bewijs in gewone taal | 4 |
| Aangehaalde Lean-schatting | 5 |
De auteurs noemen ook verschillen in een andere schatting, voor de drukflux. De versie in gewone taal gebruikt daarin een term met B_R; de Lean-versie hangt ook af van A_R. Volgens de auteurs zijn die twee grenzen moeilijk met elkaar te vergelijken.
Wat een Lean-controle wel en niet vastlegt
Lean is een bewijsassistent: software waarmee wiskundige uitspraken en bewijsstappen formeel worden vastgelegd en gecontroleerd. Een geslaagde controle bevestigt dat het gecodeerde bewijs de gecodeerde stelling volgt volgens de regels van het systeem. Op zichzelf bevestigt die controle niet dat de formele formulering inhoudelijk overeenkomt met het bewijs in gewone taal.
De auteurs stellen niet dat OpenAI’s bewijs in gewone taal onjuist is. Hun kritiek betreft de overeenkomst tussen die tekst en de onderdelen van de Lean-formalisering die zij onderzochten.
