OpenAI publiceert 722 manuscripten met wiskunderesultaten

OpenAI publiceert 722 manuscripten met wiskunderesultaten van een intern, nog niet uitgebracht model en zet de collectie op 6 oktober in een openbare GitHub-repository.

De resultaten zijn nu naast de papers en een deel van hun bewijsbestanden te inspecteren, terwijl het model zelf niet beschikbaar is. Voor Nederlandse R&D-teams die AI-leveranciers op technische claims beoordelen, verschuift de toets naar de vraag welke beweringen een uitvoerbaar bewijs ondersteunen en waar menselijke uitleg of controle nog ontbreekt.

OpenAI zet de selectie om in 722 manuscripten

In de openbare repository staan 722 manuscripten, verdeeld over 372 resultatfamilies. Een familie groepeert verwante papers: een hoofdresultaat, begeleidende argumenten, gevolgen of alternatieve bewijzen. OpenAI zegt dat het model ongeveer 4.000 problemen kreeg voorgelegd. Selectie op betekenis leverde volgens het bedrijf 372 families en 722 manuscripten op, maar de repository noemt geen meetbare selectiedrempel. Sommige teksten bouwen voort op eerder modelwerk.

De repository vergelijkt het gemiddelde rekenverbruik per resultaat met ongeveer drie uur ChatGPT Pro Thinking. Dat is geen gemeten looptijd per bewijs of gepubliceerde prijs. De repository bevat tien verkorte samenvattingen van redeneringen van het model, geen volledige verslagen voor alle manuscripten. OpenAI noemt twee uitzonderingen op de gebruikelijke werkwijze: onderzoek naar een nulvrije regio voor de Riemann-zètafunctie en een bewijs rond het vermoeden van Hodge voor CM-abelse variëteiten. De leesbare versie van de zèta-uitwerking voor Re(s) > 11/12 is door mensen geredigeerd.

Per manuscript staan citatiegegevens en bouwinstructies klaar. Correcties komen volgens OpenAI als nieuwe versies online, terwijl eerdere versies beschikbaar blijven. Zo kan een lezer wijzigingen volgen en naar de bedoelde versie verwijzen.

De claim van honderd krijgt nu materiaal

OpenAI meldde op 21 september dat zijn model ruim honderd langlopende wiskundeproblemen had opgelost. Het bedrijf kondigde toen ook een onafhankelijke adviesgroep aan die over beoordeling en communicatie van de resultaten zou adviseren. De nieuwe collectie maakt de claim concreter met papers, citatie-informatie en ondersteunende bewijsbestanden. The Verge meldt dat details over de afzonderlijke problemen en de publicatiedatum tot deze release onbekend waren.

De tellingen gebruiken verschillende eenheden: de eerdere claim telde problemen, de nieuwe catalogus manuscripten. De 722 manuscripten zijn daarom geen telling van evenveel onafhankelijk bevestigde stellingen. OpenAI zegt ook dat sommige teksten voortbouwen op eerder modelwerk.

162 papers staan in de formele catalogus

De machineleesbare Lean-catalogus koppelt 162 paperverwijzingen aan 185 hoofdresultaat-vermeldingen en specifieke bestanden. Voorbeelden zijn de symmetrische Mahler-vermoedens, tegenvoorbeelden rond Kaplansky’s quasitrace-vermoeden, optimale Max-Cut-hardheid en globale klassieke oplossingen voor het relativistische Vlasov-Maxwell-systeem. Meerdere resultaatvermeldingen kunnen dus bij één paper horen.

Lean controleert een stelling nadat die formeel in de taal is vastgelegd. De documentatie legt uit dat de kernel een bewijs accepteert binnen de stelling, definities en axioma’s van het project. Die controle zegt op zichzelf niet of de formele stelling de informele claim in de paper precies weergeeft, of het resultaat nieuw is en hoe zwaar het inhoudelijk weegt. Daarvoor moeten de vertaling, definities en literatuur ook worden gelezen.

OpenAI liet die controlelaag al zien bij de Navier-Stokes-claim waarvoor het bedrijf circa 10.000 agents en 17 uur Lean-controle rapporteerde. De nieuwe catalogus voegt een bredere reeks formele bestanden toe. Tegelijk zegt de repository dat niet alle manuscripten een Lean-formalisering hebben en dat niet-geformaliseerde resultaten problemen kunnen bevatten.

De vrijgave laat open vragen staan

OpenAI zegt de onafhankelijke adviesgroep voor wiskunde en AI te hebben geraadpleegd. De gepubliceerde aanbevelingen van die groep vragen per resultaat om de modelnaam, gebruikte prompts, een samenvatting van het redeneerproces, benodigde tijd en geraamde rekenkosten. Voor grote batches vraagt de groep ook uitleg over vergelijkbare problemen die niet zijn opgelost en over de selectie van opgaven. OpenAI deelt een gemiddelde compute-inschatting, ongeveer 4.000 voorgelegde problemen en tien verkorte samenvattingen. Individuele prompts, rekentijd en kosten per resultaat staan niet in de repository.

Scientific American meldt dat OpenAI aan de redactie vertelde dat eigen wiskundigen veel van de nieuwe resultaten nog niet begrijpen. Dat raakt een andere laag dan de Lean-check: een computer kan een formele bewijsstap toetsen, terwijl de wiskundige betekenis, de plaats in de literatuur en mogelijke toepassingen nog verder moeten worden uitgelegd. De adviesgroep vraagt AI-labs daarom ook om middelen voor begrip van complexe resultaten.

Meta kiest voor zichtbare samenwerking

Op 2 oktober publiceerde Meta zes wiskundepapers met Muse Spark. Volgens het bedrijf beantwoorden vijf daarvan open onderzoeksvragen. Meta zegt dat wiskundigen het onderzoek leidden, een tweede groep het werk beoordeelde en de papers passages markeren die vooral door onderzoekers of AI zijn geschreven. Dat is een andere herkomstketen dan OpenAI’s grotendeels modelgeproduceerde batch. De Meta-papers laten zien hoe onderzoekers AI-bijdragen en menselijke tekst afzonderlijk markeren.

OpenAI’s vrijgave vergroot wat buitenstaanders kunnen inspecteren: papers, een subset Lean-bestanden en een deel van de procesinformatie. De formele catalogus geeft per vermelding een pad naar de Lean-verklaring. De manifest markeert de scope als ‘Partial progress’ en de reviewstatus als ‘unchecked’. Voor Nederlandse R&D-afdelingen zit de directe betekenis in die bewijsketen: de claim, de formele stelling en de menselijke beoordeling zijn afzonderlijke onderdelen van een leveranciersdossier. OpenAI noemt nog geen datum waarop het interne model beschikbaar komt.