OpenAI’s Astra kraakt tien wiskundeproblemen

OpenAI koos op 1 augustus 2026 voor een opvallende manier om zijn volgende modelfamilie te presenteren. Geen persbericht, maar tien opgeloste wiskundeproblemen die de onderzoekers rechtstreeks op GitHub zetten. Onderzoeker Noam Brown maakte de resultaten van Astra bekend, de reeks die OpenAI intern als zijn nieuwe hoofdmodel ziet.

Tien open problemen, in Lean vastgelegd

Volgens het verslag van Astra gaat het om tien open vraagstukken uit de wiskunde en de theoretische informatica, verspreid over meetkunde, coderingstheorie, groepentheorie, kwantumcomplexiteit en combinatoriek. Wiskundigen boekten op geen van die problemen vooruitgang, bij de meeste al tien jaar of langer niet. OpenAI leverde de oplossingen als formele bewijzen in Lean, een taal waarin een computer elke stap kan narekenen. Daar zaten ook uitgeschreven redeneringen bij die laten zien hoe het model tot zijn antwoord kwam.

Thomas Bloom, wiskundige aan de University of Manchester, noemde de resultaten tegenover The Decoder “big news” en achtte ze zwaarder wegen dan eerdere AI-prestaties op dit vlak. Dat AI zich aan wiskundig bewijs waagt is op zich niet nieuw. Eerder wogen wiskundigen het bewijswerk van GPT-5.6 Sol Ultra, maar de omvang en de controleerbaarheid liggen nu hoger.

Meerdere agents die dagenlang doorwerken

Astra is opgezet om lange, ingewikkelde taken aan te pakken door meerdere agents te laten samenwerken. Die plannen, verdelen het werk en blijven soms uren of dagen op de achtergrond doorrekenen aan onderzoek, code en wetenschappelijke vraagstukken. OpenAI liet dat werkprincipe eerder al zien. De kosten vielen deze keer mee: alle tien de bewijzen samen kostten volgens Brown zo’n 2.000 dollar aan Sol-API-tarieven. “We hebben niet veel per probleem uitgegeven. Je kunt de rekentijd nog veel verder opvoeren”, zei hij daarover.

Wat Astra uiteindelijk gaat heten, is nog niet duidelijk. OpenAI heeft niet besloten of de reeks als GPT-6 verschijnt of als een variant binnen de GPT-5-lijn. Een releasedatum ontbreekt eveneens.

Eerst langs de Amerikaanse overheid

Astra wordt het eerste model dat het nieuwe Amerikaanse beoordelingskader moet doorlopen. Dat kader vraagt ontwikkelaars om frontier-modellen vrijwillig aan de overheid voor te leggen voordat ze breed uitkomen, met een venster van dertig dagen. De uitwerking daarvan moet eind augustus 2026 rond zijn. Eerder haalde die aanpak de deadline van 1 augustus. De timing valt daarmee samen met de release van Astra, in een markt waar concurrenten als DeepSeek intussen hun modellen voor agents en code aanscherpen.

Wat betekent dit

De keuze om resultaten in Lean te publiceren is slim gekozen: een bewijs dat een computer narekent, laat minder ruimte voor twijfel dan een demo of een benchmark-score. Voor onderzoekers is dat het interessante deel, niet zozeer welk nummer OpenAI op het model plakt. Tegelijk is Astra nog niet los. Het model gaat eerst door de overheidstoets, en pas daarna wordt zichtbaar of de wiskundeprestaties zich vertalen naar het dagelijkse werk van programmeurs en wetenschappers. Voor nu is het vooral een teken dat modellen die langer nadenken en samenwerken, aan problemen kunnen komen waar mensen jaren op vastliepen.