Lean checkt Astra’s wiskunde, peer review nog niet

OpenAI bracht deze week naar buiten dat een interne versie van zijn volgende model, Astra, tien open problemen in de wiskunde en de theoretische informatica heeft gekraakt. Het opvallende zit niet alleen in de resultaten, maar in de manier waarop het bedrijf ze aanlevert: elk bewijs komt met een machinecontrole. Dat verschuift de discussie over AI en wiskunde naar een nieuwe vraag, namelijk wie of wat een bewijs uiteindelijk goedkeurt.

Wat de machine nu wel controleert

In de blogpost “Ten advances in mathematics and theoretical computer science” beschrijft OpenAI tien resultaten die elk minstens tien jaar open stonden. Er zit een expliciete constructie van een niet-sofische groep bij, een vraag die sinds Michail Gromov het begrip soficiteit in 1999 introduceerde onbeantwoord bleef. Ook verbeterde het model een bovengrens voor sphere-packing die sinds 1978 overeind stond, en het loste drie problemen uit de catalogus van Paul Erdos op.

Belangrijker voor de controleerbaarheid: bij elk resultaat hoort een certificaat in Lean 4, gepubliceerd op de GitHub van OpenAI. De trusted kernel van Lean geeft een binair oordeel. De code compileert of niet, en iedereen kan die check zelf draaien. Dat is een ander soort zekerheid dan een tekstueel bewijs dat maandenlang op een redactie ligt. Volgens Quartz kostte het vinden van alle tien de oplossingen ongeveer 2.000 dollar aan Sol-API-tarieven, wat laat zien hoe goedkoop dit type rekenwerk inmiddels is.

Waarom wiskundigen toch op de rem trappen

Een groen licht van de Lean-kernel is niet hetzelfde als acceptatie door de vakwereld. Geen van de tien resultaten ging door peer review, en dat wringt. Thomas Bloom, de wiskundige uit Manchester die de Erdos-catalogus beheert, noemde het werk op X “big news” en zwaarder dan een eerder resultaat. Diezelfde Bloom haalde in oktober 2025 nog publiekelijk een onterechte claim van OpenAI onderuit, dus zijn instemming weegt.

De bredere zorg is eerder vastgelegd in de Leiden-verklaring van juni 2026, die de steun kreeg van de International Mathematical Union. Binnen een dag tekenden meer dan duizend mensen. De kern: alleen menselijke auteurs zijn verantwoordelijk voor de correctheid van een bewijs en voor het netjes toeschrijven van eerder werk. The Next Web wees erop dat de verklaring AI-bedrijven verwijt dat ze gepubliceerd onderzoek gebruiken, peer review omzeilen en de gebruiken rond bewijs en krediet uithollen. Die spanning over wie de eer voor een ontdekking krijgt speelt al langer.

Wat betekent dit

Astra laat zien dat de bottleneck verschuift. Het genereren van een bewijs is niet langer het lastige deel, de sociale weging ervan wel. Een Lean-certificaat pakt de logische correctheid aan, maar zegt niets over of een probleem interessant is, of de aannames kloppen, of wie de bouwstenen aandroeg. Voor wie de context wil: eerder beschreven we hoe Astra tien wiskundeproblemen kraakte en hoe het model dagenlang aan een taak doorwerkt. OpenAI deelt intussen ook rekentijd met de academische wereld, zoals bij het programma voor onderzoekers. De komende maanden draait het om iets simpels: gaan specialisten deze tien bewijzen echt nalopen, of blijft het bij een persbericht met een groene compilatie.