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.
