OpenAI: tien wiskundige resultaten geformaliseerd in Lean en de rol van het interne model

Op 1 augustus publiceerde OpenAI het manuscript “Ten Advances in Mathematics and Theoretical Computer Science” en schreef de resultaten toe aan een eigen intern model. Tegelijk verscheen de GitHub-repository `openai/ten-proofs`, die de Lean 4-formalisaties van alle tien bewijzen beschikbaar maakt. Onder de resultaten springen eruit: een betere exponent voor het stapelen van bollen — de eerste sinds 1978 —, de constructie van een niet-sofische groep en een tegenvoorbeeld bij het rigiditeitsvermoeden van Connes. De repository is een Lean 4.32.0-project op basis van mathlib, uitgebracht onder Apache-2.0: iedereen kan de bewijzen hercompileren met `lake exe cache get` en `lake build All`, en een map ComparatorChallenges legt uit hoe je de verificatie onafhankelijk uitvoert.

De berichtgeving heeft deze resultaten gekoppeld aan “Astra”, de naam van de volgende modelfamilie die OpenAI op diezelfde 1 augustus aankondigde; het manuscript spreekt echter alleen over “een intern model”, dat niet is vrijgegeven. Gegevens als de circa 2.000 dollar aan tokens of de 249 pagina's van het document komen uit berichtgeving van derden, want de officiële aankondigingspagina is momenteel onbereikbaar. Het paper bedankt menselijke wiskundigen voor het meelezen en wijst op onafhankelijk, gelijktijdig werk van Shuoxing Zhou, deels tot stand gekomen met hulp van GPT-5.6 Sol.

Volgens SiliconANGLE komen de wiskundige argumenten van het model, maar waren het menselijke onderzoekers die de output tot publiceerbare manuscripten maakten: hoe zwaar dat bijschaven weegt, is niet becijferd. Het gebruik van Lean 4 verlegt het debat: een certificaat garandeert de logische geldigheid van het bewijs, maar bevestigt niet automatisch dat de geformaliseerde stelling samenvalt met het historische open probleem — die controle blijft mensenwerk. Geen van de tien resultaten heeft formele peer review doorlopen. Het precedent weegt: in oktober 2025 bleek de aankondiging dat GPT-5 tien Erdős-problemen had “opgelost” ongegrond, en Thomas Bloom, beheerder van erdosproblems.com, noemde het een ernstige verkeerde voorstelling van zaken. Over de tien resultaten van vandaag spreekt diezelfde Bloom juist van “big news”. Zoals theoretisch fysicus Tobias J. Osborne opmerkt, zijn de genoemde 2.000 dollar de kosten van de winnende tokens, niet de totale oogst van alle pogingen — een cijfer waarover OpenAI niets heeft gezegd. Dit alles speelt tegen de achtergrond van de “Leiden Declaration on Artificial Intelligence and Mathematics”, gepubliceerd in juni 2026 en volgens the-decoder gesteund door meer dan 3.000 wiskundigen en door de International Mathematical Union, die vraagt om transparantie, bescherming van auteursrechten en menselijke verantwoordelijkheid voor de resultaten.

Het echte nieuws is niet dat een machine wiskunde heeft bedreven — dat gebeurt al maanden — maar dat elk resultaat deze keer komt met een hercompileerbaar Lean-certificaat: om te oordelen hoef je degene die het aankondigt niet te geloven. Zolang de verhouding tussen mislukte pogingen en successen echter een bedrijfsgeheim blijft, blijft het beoordelen van de efficiëntie van deze modellen eerder een geloofskwestie dan statistiek.