OpenAI publikuje 722 prace matematyczne z niewydanego modelu

Co dokładnie opublikowało OpenAI

Materiał trafił do repozytorium openai/math na GitHubie, a firma zapowiedziała go wpisem „Sharing AI progress in mathematics”. Według opisu repozytorium są to manuskrypty i artefakty dowodowe przygotowane przez wewnętrzny model OpenAI w ramach ewaluacji na otwartych problemach badawczych. Firma rozszerzyła takie testy, gdy model zaczął osiągać maksymalne wyniki w dotychczasowych sprawdzianach matematycznych.

Rodzina wyników to grupa powiązanych prac: główny rezultat, argumenty pomocnicze, wnioski albo alternatywne dowody. Każdą rodzinę przypisano do dyscypliny, a całość opisuje osobny dokument przeglądowy. Dla dziesięciu wybranych wyników OpenAI udostępniło też skrócone podsumowania rozumowania modelu.

OpenAI nie podało nazwy modelu ani terminu jego udostępnienia. Scientific American przekazuje, że firma pracuje nad odpowiedzialnym wydaniem modelu, który wygenerował te wyniki.

Jak model doszedł do wyników

Według repozytorium zdecydowaną większość wyników uzyskano jedną, stałą procedurą. Model dostał w sumie ok. 4 tys. problemów, a na jeden wynik przypadały średnio trzy godziny obliczeń w trybie myślenia ChatGPT Pro. Katalog powstał po zgrupowaniu rezultatów w rodziny i odrzuceniu tych, które nie spełniły progu znaczenia naukowego.

Firma wskazuje dwa wyjątki od tej procedury: pracę nad obszarem bez zer funkcji dzeta Riemanna i dowód hipotezy Hodge'a dla rozmaitości abelowych typu CM. Opis wyniku dla funkcji dzeta zredagowali dodatkowo ludzie, aby poprawić czytelność. Scientific American zwraca uwagę na kontrast z wcześniejszym ogłoszeniem OpenAI dotyczącym równań Naviera-Stokesa, przy którym według redakcji pracował rój ok. 10 tys. agentów.

Ile wyników ma formalny dowód

Lean to asystent dowodzenia, czyli język programowania, w którym komputer sprawdza każdy krok dowodu. Wynik sformalizowany w Lean jest bardzo mało prawdopodobny do obalenia, o ile poprawnie zapisano samo twierdzenie. Sprawdziliśmy plik formalization.yaml w repozytorium. Stan na 7 października 2026 roku wygląda tak:

• 722 manuskrypty w katalogu, 372 rodziny wyników,
• 162 prace z głównym wynikiem wpisanym do katalogu formalizacji w Lean,
• status projektu formalizacji: częściowy postęp (Partial progress),
• przegląd formalizacji: oznaczony jako niesprawdzony (unchecked),
• OpenAI zapowiada dodawanie kolejnych formalizacji i zachowanie historii wersji z poprawkami.

Jak reagują matematycy

Środowisko jest podzielone. Andrew Sutherland z MIT powiedział Scientific American, że do czasu udostępnienia modelu wszystkie takie deklaracje należy traktować jako niezweryfikowane. Daniel Litt z Uniwersytetu w Toronto argumentuje odwrotnie: skoro wyniki istnieją, nie ma powodu, by firma trzymała je w tajemnicy.

Terence Tao krytykował wcześniej tempo, w jakim laboratoria AI publikują wyniki matematyczne. Problem jest praktyczny: sprawdzenie setek prac wymaga miesięcy pracy specjalistów. We wrześniu 2026 roku OpenAI powołało niezależną grupę doradczą ds. matematyki, która zaleciła ujawnianie modeli, poleceń i czasu obliczeń. Według Scientific American firma zobowiązała się do podania średniego czasu obliczeń i wybranych statystyk, ale nie ujawniła poleceń.

Ograniczenia i niewiadome

Repozytorium to materiał firmy, która rozwija własny model, a prace nie przeszły recenzji w czasopismach. Przed powoływaniem się na te wyniki trzeba uwzględnić kilka zastrzeżeń:

• OpenAI samo przyznaje, że część niesformalizowanych wyników może mieć błędy, i zapowiada szybkie poprawki.
• Nie wiadomo, ile z ok. 4 tys. problemów model nie rozwiązał ani jak dokładnie wyglądały polecenia.
• Formalizacja w Lean potwierdza poprawność dowodu, ale nie przesądza o nowości wyniku ani o tym, czy ktoś nie rozwiązał problemu wcześniej.
• Model nie jest publicznie dostępny, więc niezależni badacze nie mogą odtworzyć procesu.
• Kwestia przypisania autorstwa pozostaje otwarta. Wszystkie formalizacje podpisano jako OpenAI, bez nazwisk osób, które przygotowywały manuskrypty.

Co to oznacza dla polskich badaczy

W naszej ocenie najważniejsza zmiana dotyczy skali. Meta opisała niedawno sześć prac powstałych przy współpracy matematyków z modelem, a OpenAI publikuje ponad 700 manuskryptów bez ludzkich współautorów. Dla polskich zespołów badawczych to sygnał, że przegląd literatury przed publikacją musi obejmować także takie repozytoria, a nie tylko arXiv i czasopisma.

Badacz, który pracuje nad problemem z jednej z opisanych dziedzin, powinien sprawdzić plik CONTENTS.md w repozytorium. Jeśli znajdzie tam swój problem, warto porównać podejście i sprawdzić, czy wynik ma formalizację w Lean. Prace można cytować według bloków BibTeX dołączonych do każdego manuskryptu, ale do czasu recenzji lepiej opisywać je jako niezweryfikowane preprinty.