In wat alleen maar kan worden omschreven als het academische equivalent van iemand een piano op zijn hoofd laten vallen en hem dan vragen de bladmuziek te recenseren, heeft OpenAI deze week bijna 400 door AI gegenereerde wiskundige resultaten vrijgegeven, verspreid over meer dan 700 manuscripten. De reactie vanuit de wiskundegemeenschap varieerde van "verbijsterend" tot "pure waanzin" – en dat waren nog de beleefde reacties.

De verzameling bestrijkt combinatoriek, verschillende takken van de meetkunde, getaltheorie, theoretische informatica, algebra, topologie, kansrekening en statistische mechanica, en mathematische fysica. Het is zo omvangrijk dat OpenAI zich genoodzaakt voelde richtlijnen te publiceren over hoe je door de uitgestrekte GitHub-repository navigeert, wat een beetje lijkt op iemand een plattegrond geven van een gebouw dat je net in brand hebt gestoken.

"Alleen al het doornemen van de volledige lijst met samenvattingen is overweldigend," zei Álvaro Lozano-Robledo, hoogleraar wiskunde aan de Universiteit van Connecticut. Verschillende wiskundigen vertelden The Verge dat het simpelweg doorwerken van de ongeveer 40 pagina's tellende inhoudsopgave en samenvattingen hen het grootste deel van een uur kostte. Voor wie de score bijhoudt: dat is één uur alleen al om het menu te lezen.

Verspreid tussen de honderden manuscripten bevinden zich formalisaties in Lean, een programmeertaal en bewijsassistent waarmee resultaten computationeel kunnen worden geverifieerd. Deze formalisaties zijn van cruciaal belang gebleken bij het beoordelen van enkele eerdere wiskundige claims van OpenAI, waardoor onderzoekers erop kunnen vertrouwen dat een bewering logisch correct is, zelfs als ze het argument erachter niet volledig begrijpen – wat een beetje lijkt op een rekenmachine vertrouwen zonder te weten wat delen is.

Maar de mate waarin elk resultaat was geverifieerd, varieerde enorm. Op GitHub erkende OpenAI dat de resultaten "zich in verschillende stadia van verificatie bevinden" en dat "veel, maar niet alle, manuscripten zijn geformaliseerd." Op het moment van schrijven lijken minder dan de helft van de manuscripten in de verzameling formeel te zijn beschreven. OpenAI zei dat slechts 300 topresultaten van de 719 manuscripten waren geformaliseerd – ongeveer 42 procent – en dat het "de repository zal bijwerken met meer formalisaties zodra we die verkrijgen." Dus ruwweg 58 procent van de wiskundige apocalyps blijft ongeverifieerd. Slaap lekker.

Verschillende wiskundigen klaagden bij The Verge over het gebrek aan formalisatie, vooral gezien het enorme aantal resultaten. Zelfs wanneer Lean-code een resultaat vergezelt, is de evaluatie niet onmiddellijk. Onderzoekers moeten controleren of de formalisatie daadwerkelijk bewijst wat het resultaat beweert – nog een tijdrovend proces. Verschillenden die de papers doornamen, zeiden dat zelfs waar computerverifieerbare bewijzen waren geleverd, de kwaliteit inconsistent was en de beweringen die ze verifieerden niet altijd netjes leken overeen te komen met de claims in de begeleidende manuscripten.

Kevin Buzzard, hoogleraar wiskunde aan Imperial College London, zei dat hij talrijke stellingen in zijn vakgebied – de algebraïsche getaltheorie – had geïdentificeerd, waarvan er slechts ongeveer zes onmiddellijk "in het oog sprongen." Weinigen, zo niet geen, van die leken formeel geverifieerd in Lean. "Daarom moet ik ofwel mogelijk onjuiste troep lezen, of wachten tot anderen hetzelfde doen, of wachten tot iemand ze formaliseert voordat ik zeker kan zeggen dat de resultaten überhaupt correct zijn." Buzzards zorgen werden weerspiegeld door talrijke andere onderzoekers, die vermoedelijk deze week wel iets beters te doen hadden.

Buzzard was zeker niet de enige die zich zorgen maakte over AI-"troep" – een afkorting voor materiaal van lage kwaliteit, vaak foutief gegenereerd door AI, dat steeds vaker opduikt online en in de echte wereld, inclusief academische papers. Zoals in andere vakgebieden vertelden wiskundigen aan The Verge dat ze de afgelopen jaren een enorme toename hebben gezien van dergelijk materiaal geproduceerd met tools zoals ChatGPT en Claude. Veel ervan is verwarrend, moeilijk leesbaar en getuigt van weinig begrip van het onderwerp; het is bijzonder schamel als het gaat om het erkennen van andere onderzoekers. Eerdere wiskundige publicaties van OpenAI werden breed bekritiseerd door experts vanwege