OpenAI har lagt ut 719 matematiska manuskript från en intern AI-modell i ett offentligt GitHub-arkiv. Manuskripten är ordnade i 372 grupper med besläktade arbeten. OpenAI beskriver resultaten som forskning från modellutvecklingen, inte som färdigverifierade bevis.
Vad innehåller arkivet?
Ämnena sträcker sig från talteori till fysik och datavetenskap. Bland exemplen finns arbeten om pi:s irrationalitetsexponent, Hodge-förmodan för vissa abelska varieteter och kvantmagnetism. Arkivet innehåller förtryck, källfiler och stödmaterial för enskilda manuskript.
OpenAI skriver att den övervägande delen av resultaten togs fram med samma metod och en ännu inte offentliggjord intern modell. I genomsnitt användes tre timmar av ChatGPT Pro-tänkberäkning per resultat. Modellen fick omkring 4 000 problem under utvärderingen; ett urval av resultaten sattes sedan samman till manuskript och grupper.
Hur mycket är kontrollerat?
OpenAI säger att ungefär 42 procent av huvudresultaten har formaliserats i Lean, ett verktyg för att kontrollera matematiska bevis. Företaget betonar att samlingen innehåller resultat på olika verifieringsstadier och att vissa ännu saknar sådana formaliserade bevis. Det varnar också för att en del oformaliserade resultat kan innehålla fel.
Det finns undantag från den beskrivna arbetsmetoden, bland annat arbetet om ett nollfritt område för Riemanns zetafunktion och beviset av Hodge-förmodan för CM-abelska varieteter. Texten om ett nollfritt område där realdelen är större än 11/12 redigerades dessutom av en människa för att bli mer lättläst.
Varför det spelar roll
Matematiker kan läsa manuskripten och granska tillhörande filer, men OpenAI uppger att en stor del av huvudresultaten ännu saknar formella Lean-bevis. Därför går det inte att behandla hela samlingen som kontrollerad enbart för att den ligger i ett offentligt arkiv; hur många oformaliserade resultat som håller är inte fastställt i källan.
