OpenAI opublikowało 722 manuskryptów matematycznych stworzonych przez niewydany wewnętrzny model, opisując tę pracę jako efekt procesu opartego w większości na jednym prompcie i jednym agencie. Artykuły są uporządkowane w 372 rodziny powiązanych wyników, ale matematycy twierdzą, że tych twierdzeń nie można w pełni ocenić, dopóki model, prompty i dodatkowe dowody nie zostaną udostępnione.

Publikacja pojawia się w momencie, gdyatoria AI coraz częściej wykorzystują matematykę jako poligon doświadczalny dla rozumowania modeli frontowych i staje się wczesnym testem tego, jak badania generowane przez AI powinny być publikowane, sprawdzane i ujawniane.

Rzecznik OpenAI powiedział, że niemal wszystko powstało z pojedynczego promptu przekazanego jednemu agentowi AI, choć niektóre wyniki mogły wymagać wielu prób. Firma oświadczyła, że przedstawiła modelowi około 4 000 problemów i wybrała te wyniki, które uznała za na tyle istotne, by je opublikować.

Andrew Sutherland, matematyk z MIT, powiedział Scientific American, że tezę o rozwiązaniu jednym strzałem należy traktować ostrożnie. „Dopóki nie wydadzą modelu i ludzie nie będą mogli powtórzyć ich wyników, uważam, że wszelkie twierdzenia o rozwiązywaniu problemów jednym strzałem za pomocą jednego agenta należy traktować jako niezweryfikowane” – powiedział Sutherland. „Powinniśmy żądać dowodów”.

Liczba 722 oznacza manuskrypty, a nie rozwiązane problemy. Rodzina wyników może zawierać główne twierdzenie wraz z argumentami towarzyszącymi, wnioskami lub alternatywnymi dowodami. OpenAI oświadczyło, że przeciętny wynik zużył odpowiednik około trzech godzin mocy obliczeniowej trybu myślenia ChatGPT Pro. To różni się od ubiegłomiesięcznego twierdzenia firmy dotyczącego równań Naviera-Stokesa, które angażowało 10 000 koordynujących się agentów pracujących przez 88 godzin.

OpenAI opublikowało skrócone podsumowania rozumowania dla 10 wyników. Jednak katalog formalizacji w repozytorium na GitHubie pokazuje, że tylko 162 z 722 manuskryptów zawiera obecnie komputerowo sprawdzony wynik główny. To około 22% kolekcji i oznacza, że wynik został przetłumaczony na Lean – oprogramowanie mechanicznie sprawdzające każdy krok logiczny. Lean stał się standardem pracy dla dowodów sprawdzanych maszynowo w matematyce, dlatego około 560 wciąż niesformalizowanych manuskryptów stanowi główną otwartą kwestię tej kolekcji.

OpenAI przyznało, że nie wszystkie manuskrypty mają formalizacje w Lean, i ostrzegło, że „niektóre niesformalizowane wyniki mogą zawierać problemy”. Pomyślna wfikacja w Lean potwierdza jedynie, że dowód wynika ze zdania zapisanego w Lean. Nie dowodzi, że zdanie odpowiada oryginalnemu problemowi ani że wynik jest nowy lub istotny. Te kwestie nadal wymagają oceny matematyków.

Badacze wyrazili już obawy dotyczące materiału i sposobu jego publikacji. Dmitry Rybin napisał na X:

I was trying to read the OpenAI proof that chromatic number of a plane is >= 6. But it is totally unbelievable alien math? Somehow the model found that any K-coloring <=> "weakly measurable" K-coloring, which seems out of nowhere 1/2 pic.twitter.com/W13ScT3nel — Dmitry Rybin (@DmitryRybin1) October 7, 2026

Keith Adler napisał na X:

The openai/math repo has Issues turned off and has never accepted a pull request. That's disappointing. If you publish 722 manuscripts and ask for Lean formalisations, you need somewhere for people to send them. I'm formalising OpenAI's Saxl's Conjecture proof in Lean 4 against… — Keith Adler (@keithadler) October 7, 2026

Institute for Advanced Study w Princeton w stanie New Jersey również zakwestionowało implikacje matematycznej pracy generowanej przez AI. „Obecnie AI może generować argumenty matematyczne w sytuacjach, w których człowiek, który je wywołał, nie jest w stanie ich zrozumieć, zweryfikować ani wziąć za nie odpowiedzialności” – oświadczył instytut. „Wierzymy, że ludzkie rozumienie matematyki pozostaje sprawą najwyższej wagi. Jak w tej nowej erze możemy dążyć do nowego paradygmatu, w którym ludzkie rozumienie matematyki będzie częścią odpowiedzialnego dorobku naukowego?”

Profesor Abhishek Saha przyjął bardziej pozytywne stanowisko, pisząc: „To bardzo ważny dzień dla matematyki”. Stwierdził, że większość wyników mieści się w kategoriach takich jak „wyjątkowe postępy w ramach istniejącego programu” i „zaskakujące przełomy”. Jego zdaniem kolekcja zawiera interesujące problemy, ale nie wyniki porównywalne z problemami milenijnymi – siedmioma nagrodzonymi milionem dolarów pytaniami Clay Mathematics Institute. Wskazał hipotezę quasi-Riemanna jako jedyny z 722 wyników osiągający ten poziom znaczenia.

Saha napisał na X:

Some further thoughts on the 372 results released by OpenAI today, across 722 manuscripts. If I were to classify theorems that mathematicians prove and publish according to their groundbreaking nature, I would (very roughly) divide them into four categories: A) Non-breakthrough… — Abhishek Saha (@ObhishekSaha) October 7, 2026

Publikacja nie speniła także zaleceń wydanych 29 września przez grupę doradczą Institute for Advanced Study. Grupa zaleciła ujawnienie nazwy modelu, promptów, podsumowanego łańcucha rozumowania, czasu trwania i kosztu obliczeniowego każdego wyniku. OpenAI dostarczyło średnie dane obliczeniowe i 10 podsumowań rozumowania, ale nie prompty. Firma oświadczyła, że nadal pracuje nad odpowiedzialnym udostępnieniem modelu.

Daniel Litt, matematyk z University of Toronto, zajął przeciwne stanowisko i argumentował, że nie ma powodu, by żądać od OpenAI utrzymywania w tajemnicy odpowiedzi na te pytania matematyczne.

Anthropic obrał inny podejście w ubiegłym miesiącu, publikując na GitHubie wszystkie 13 milionów linii zweryfikowanego w Lean dowodu Wielkiego Twierdzenia Fermata. Ta praca sformalizowała twierdzenie opublikowane przez Andrew Wilesa w 1995 roku, zamiast przedstawiać nowe wyniki matematyczne. Obie publikacje ilustrują podział w strategii ujawniania informacji w całej branży: z jednej strony kompletny, sprawdzony maszynowo dowód znanego twierdzenia, z drugiej – duża partia nowych twierdzeń z częściową formalną weryfikacją.

OpenAI oświadczyło, że będzie dodawać formalizacje w Lean w miarę ich uzyskiwania. Na razie 162 z 722 manuskryptów ma sformalizowany wynik główny. Pozycja reszty zależy teraz od tego, czego badacze potrzebują najbardziej: wydania modelu, leżących u podstaw promptów oraz niezależnych formalizacji pozostałych manuskryptów.