Az OpenAI egyszerre 719 matematikai kéziratot és a hozzájuk tartozó bizonyítási anyagokat tett nyilvánossá. A gyűjteményt egy kiadatlan belső modell állította elő: az OpenAI szerint körülbelül négyezer nyitott problémát adott neki, egy-egy eredményhez pedig átlagosan háromórányi ChatGPT Pro-számítás jutott.
A mennyiség önmagában nem jelenti, hogy 719 új, ellenőrzött tétel született. A kéziratok 372 családba rendeződnek, mert egy eredményhez fő állítás, következmény, kiegészítő érv vagy alternatív bizonyítás is tartozhat. Az OpenAI azt is jelzi, hogy az anyagok az ellenőrzés különböző szakaszaiban vannak, a formális Lean-bizonyítás pedig a fő eredmények körülbelül 42 százalékához készült el.
A Lean-kód géppel ellenőrizhetővé teheti, hogy egy formális állítás következik-e a megadott alapokból, de nem dönti el automatikusan, hogy a kód pontosan ugyanazt állítja-e, mint a kézirat, helyes-e a szakirodalmi előzmények bemutatása, vagy fontos-e az eredmény. A The Verge több mint harminc matematikussal beszélt; a korai reakciók között lelkesedés és erős aggodalom egyaránt volt, a hiányos formalizálás és a nehezen olvasható szövegek miatt.
Az OpenAI matematikaügyi tanácsadó csoportja, az AGMAI is úgy fogalmazott: a nyilvánosságra hozatal csak a kezdet. Korábbi ajánlásuk szerint az AI-laboroknak fel kellene tárniuk a használt modellt, a promptokat és a számítási költséget, továbbá támogatniuk kellene az emberi ellenőrzést. A mostani repó az eljárásról és az átlagos számításról közöl adatokat, de a modell nevét nem.
A tudományos érték ezért nem egyetlen látványos darabszámban van. A következő munka annak megállapítása, mely állítások helyesek, melyek újak, hogyan kapcsolódnak a korábbi eredményekhez, és melyeket tudja a közösség érthető matematikává alakítani.
Források: OpenAI – a matematikai gyűjtemény; AGMAI – állásfoglalás az OpenAI kiadásáról; The Verge – matematikusok első értékelése.