OpenAI heeft op 1 augustus zijn volgende grote modelfamilie Astra onthuld. Volgens het bedrijf heeft een interne versie van Astra tien hardnekkige open problemen in de wiskunde en de theoretische informatica opgelost.
Belangrijkste punten:
- OpenAI bevestigde de naam Astra in een rapport dat het model crediteert met tien resultaten op problemen waar minstens tien jaar niemand meer aan had gesleuteld.
- De lijst bevat onder meer een constructie van niet-sofische groepen, een weerlegging van Connes’ rigiditeitsvermoeden en drie problemen uit de Erdős-catalogus.
- Elk argument wordt geleverd met een door machines verifieerbaar Lean-certificaat; de tokenkosten bedroegen circa 2.000 dollar tegen Sol-API-tarieven.
Rapport over OpenAI Astra somt tien wiskundige doorbraken op
Het bedrijf publiceerde zaterdag een rapport van 249 pagina’s over onder meer bolverpakkingen, coderingstheorie, complexiteit van rekenkundige circuits, groepentheorie, kwantumcomplexiteit en roostercryptografie.
Elk probleem op de lijst kende minstens tien jaar geen voortgang op het kernresultaat, en in veel gevallen was de impasse aanzienlijk langer. Een van de constructies toont het bestaan aan van niet-sofische groepen, en beslecht daarmee een centrale vraag in de groepentheorie.
Andere resultaten omvatten een weerlegging van Connes’ rigiditeitsvermoeden, een bewijs van Ehrharts volumevermoeden en de oplossing van drie problemen uit de Erdős-catalogus, waaronder een lagere grens voor meerkleurige driehoeks-Ramseygetallen. OpenAI schat de tokenkosten voor het vinden van alle tien oplossingen op ongeveer 2.000 dollar tegen Sol-API-tarieven.
Astra is opgebouwd rond meerdere ‘agents’ die één complexe taak opsplitsen, langdurig parallel werken en hun bevindingen samenvoegen. De modelfamilie komt naast de Sol-, Terra- en Luna-modellen die het label GPT-5.6 dragen. OpenAI heeft nog niet beslist of Astra als GPT-6, als GPT-5.7-variant of als aparte productlaag wordt gelanceerd, en er is geen releasedatum bekendgemaakt.
Ook interessant: Bitcoin-ETF’s trekken 233,1 miljoen dollar aan, één fonds neemt leeuwendeel voor zijn rekening
Wiskundigen beoordelen Astra’s Lean-bewijzen
Thomas Bloom, wiskundige aan de University of Manchester en beheerder van de Erdős-problemencatalogus, noemde de resultaten op X “groot nieuws”. Hij zet ze qua constructieve inhoud hoger dan het unit-distance-tegenrevoorbeeld dat OpenAI in mei publiceerde.
Elk argument wordt ondersteund door een Lean-certificaat dat door bewijsassistenten automatisch is te controleren – een lat waar tot nu toe weinig AI-claims over wiskundige doorbraken aan voldeden. Wiskundigen moeten wel nog nagaan of elke formele formulering daadwerkelijk overeenkomt met de problemen die de gemeenschap als “open” beschouwde. Noam Brown, die aan de redeneermethoden achter het systeem werkte, schreef dat er geen Millennium Prize-problemen zijn gekraakt.
Sam Altman presenteerde Astra in Washington
Sam Altman presenteerde Astra achter gesloten deuren aan senatoren en hoge regeringsfunctionarissen in Washington, enkele dagen voordat het rapport verscheen.
Hij sprak woensdag onder anderen met de senatoren Raphael Warnock en Bernie Moreno. Op zijn agenda stonden verder ontmoetingen met Mark Warner, minister van Financiën Scott Bessent en minister van Handel Howard Lutnick.
Astra wordt naar verwachting het eerste model dat wordt ingediend onder een gepland federaal toetsingskader voor AI-modellen vóór marktintroductie.
OpenAI volgde in mei een vergelijkbare route toen het bedrijf via een blogpost, en niet via een wetenschappelijk tijdschrift, een door AI gegenereerde weerlegging van het unit-distancevermoeden van Erdős aankondigde. In juni antwoordden wiskundigen met de Leidendeclaratie, een door de International Mathematical Union gesteunde waarschuwing tegen ‘proof by press release’, waar OpenAI zaterdag expliciet naar verwees.
Lees ook: Polymarket-handelaars geven Spider-Man 91% kans op historisch debuut
