OpenAI meldt dat zijn nog niet uitgebrachte model Astra tien wiskundige raadsels kraakt. Elk probleem stond al minstens tien jaar open. Het bedrijf publiceerde een manuscript van 249 pagina’s op GitHub. Daarbij levert het voor elk resultaat een machinaal controleerbaar Lean 4-certificaat. De totale rekenkosten bedroegen ongeveer 2.000 dollar. Dat bedrag is opvallend laag voor zulke resultaten.
Het opvallendste resultaat is de eerste expliciete constructie van een niet-sofische groep. Die vraag hield groepentheoretici bezig sinds Mikhail Gromov het begrip in 1999 introduceerde. Astra weerlegde daarnaast het rigiditeitsvermoeden van Connes over von neumann-algebra’s. Ook bewees het model het volumevermoeden van Ehrhart en loste het drie problemen van Paul Erdős op. Verder verbeterde het voor het eerst sinds 1978 de bovengrens voor hoogdimensionale bolstapeling. Het bewees bovendien een parallelle-herhalingsstelling voor quantumspellen met twee spelers en vond nieuwe ondergrenzen voor de circuitcomplexiteit van de permanent.
De aankondiging valt midden in een oplopend conflict tussen AI-bedrijven en wiskundigen. In juni presenteerden zij de Leidse Verklaring, gesteund door de Internationale Wiskunde Unie. Die waarschuwt dat AI-bedrijven gepubliceerd onderzoek zonder toestemming gebruiken en peer review omzeilen. Sebastien Bubeck, hoofd wiskundeonderzoek bij OpenAI, noemt de resultaten prachtig. Thomas Bloom van de erdosproblems-website spreekt van groot nieuws. In mei weerlegde dezelfde modelfamilie al een tachtig jaar oud vermoeden van Erdős. Fields-medaillewinnaar Tim Gowers wilde dat bewijs toen meteen aanbevelen voor publicatie.
De Lean-certificaten nemen een belangrijk bezwaar weg. Iedereen met de Lean-compiler kan de bewijzen zelf controleren, zonder OpenAI te vertrouwen. OpenAI geeft daarnaast 100.000 academische onderzoekers tot 2027 gratis toegang tot zijn beste modellen. Die stap versterkt de banden met de wetenschap, maar concentreert onderzoek op één platform. Wanneer Astra uitkomt, blijft onduidelijk; het bedrijf noemt het enkel zijn volgende grote model. Sommige waarnemers vermoeden dat Astra de GPT-6-reeks is. Of wiskundigen resultaten uit een blogpost accepteren, moet nog blijken.
