OpenAI publikuje setki prac matematycznych na GitHubie. Formalny dowód to nie to samo co przełom

OpenAI udostępniło w serwisie GitHub publiczne repozytorium z pracami matematycznymi wygenerowanymi przez wewnętrzny model AI. Zbiór obejmuje 722 manuskrypty pogrupowane w 372 rodziny wyników — pojedyncza rodzina zawiera zazwyczaj rezultat główny, lematy pomocnicze, wnioski lub alternatywne warianty dowodu. Firma przedstawia te prace jako rozwiązania problemów otwartych bądź postęp w ich badaniu, wymieniając m.in. zagadnienia algorytmiczne i wątki powiązane z hipotezą Riemanna.

Zamiast kierować artykuły do tradycyjnych czasopism naukowych, OpenAI opublikowało teksty wraz z historią zmian, odnośnikami bibliograficznymi oraz ogólnym opisem przyjętej metody. Firma deklaruje, że zdecydowana większość wyników powstała po pojedynczym poleceniu skierowanym do jednego agenta, a średni czas pracy modelu wynosił około trzech godzin obliczeń w trybie ChatGPT Pro Thinking. Repozytorium zawiera także szacunki kosztów, ale nie przypisano ich do poszczególnych wyników, nie ujawniono również promptów wykorzystanych do wygenerowania konkretnych prac.

Sprawdzalność kodu a waga odkrycia

Dla wielu manuskryptów — choć nie dla wszystkich — OpenAI dołączyło formalizacje w języku Lean. To narzędzie pozwalające na maszynowe sprawdzenie, czy ciąg wnioskowań w dowodzie nie zawiera błędów logicznych. Taki zapis eliminuje konieczność ręcznego sprawdzania każdego kroku pod kątem elementarnej poprawności.

Formalna weryfikacja w Lean ma jednak ściśle określony zakres. Potwierdza wyłącznie to, że dowód jest spójny i wolny od luk dedukcyjnych. Samodzielnie nie odpowiada na kluczowe dla matematyków pytania: czy dany wynik jest rzeczywiście nowy, czy problem był istotny oraz czy zaproponowana metoda wnosi nowe zrozumienie do danej dziedziny.

Wszystkie opublikowane rezultaty pozostają na razie jednostronnymi deklaracjami OpenAI. O tym, czy repozytorium stanowi realny wkład w naukę, zdecyduje dopiero środowisko akademickie po niezależnej analizie merytorycznej wartości i oryginalności przedstawionych prac.