Astra od OpenAI rozwiązała 10 problemów matematycznych

OpenAI opublikowało 1 sierpnia 2026 wpis zatytułowany „Ten advances in mathematics and theoretical computer science“, czyli dziesięć osiągnięć w matematyce i informatyce teoretycznej. Za wynikami stoi Astra, wewnętrzna wersja niewydanego jeszcze modelu następnej generacji. Część problemów była otwarta od dekad.

Najciekawsze w tym ogłoszeniu nie jest jednak samo „AI robi matematykę“. Ciekawe jest to, że po raz pierwszy przy takiej deklaracji można automatycznie sprawdzić, czy model nie zmyśla. My to zrobiliśmy.

Co konkretnie padło

Te dziesięć wyników to nie jest jedna kategoria. Pięć z nich to pełne rozstrzygnięcia albo obalenia hipotez, reszta to poprawki wcześniejszych oszacowań. Kilka przykładów, żeby dało się wyczuć skalę:

• Hipoteza soficzności. Pytanie postawił Benjamin Weiss w 2000 roku: czy każdą grupę, czyli abstrakcyjny zbiór działań z regułami składania, da się przybliżyć skończonym układem. Astra pokazała konkretny przypadek, w którym się nie da. Pytanie żyło 26 lat.
• Hipoteza sztywności Connesa. Wyrosła z twierdzenia Alaina Connesa z 1980 roku i figurowała jako Problem 1 w jego monografii z 1994. Została obalona kontrprzykładem.
• Hipoteza objętościowa Ehrharta z 1964 roku. Sam Ehrhart udowodnił ją dla płaszczyzny, tutaj padł dowód dla dowolnej liczby wymiarów.
• Wielokolorowe liczby Ramseya. To problem Paula Erdősa, za którego rozwiązanie sam wyznaczył nagrodę 250 dolarów. Astra ustaliła, jak szybko rosną te liczby.
• Upakowanie sfer w wielu wymiarach, czyli pytanie o najgęstsze ułożenie kul bez zachodzenia na siebie. Praca podaje, że to pierwsza poprawa ogólnego oszacowania od 1978 roku.

Doszły do tego wyniki z informatyki teoretycznej, między innymi dotyczące trudności obliczeniowej problemu, na którym opiera się kryptografia odporna na komputery kwantowe.

Dlaczego tym razem da się to sprawdzić

Przy większości głośnych deklaracji o AI zostaje nam wiara w komunikat producenta. Tutaj jest inaczej, bo każdy z dziesięciu dowodów model zapisał dodatkowo w Lean. To język, w którym twierdzenie zapisuje się tak, żeby komputer prześledził każdy krok rozumowania. Dowód albo przechodzi weryfikację, albo nie. Nie ma miejsca na zdanie, które brzmi przekonująco, a niczego nie dowodzi, czyli na matematyczny odpowiednik halucynacji.

OpenAI wystawiło te zapisy publicznie w repozytorium openai/ten-proofs na wolnej licencji Apache 2.0. Pobraliśmy je i policzyliśmy sami:

• 548 215 linii dowodów w jedenastu plikach,
• zero zaślepek, czyli miejsc, w których autor wstawia znacznik „tego kroku nie umiem udowodnić“ i idzie dalej,
• zero dołożonych założeń, których weryfikator nie sprawdza, i zero obejść zastępujących dowód obliczeniem.

W praktyce znaczy to tyle: żeby uwierzyć w poprawność tych dowodów, nie musisz ufać OpenAI. Wystarczy, że ufasz weryfikatorowi, a ten jest niezależnym, otwartym narzędziem, którego matematycy używają od lat. Pytanie, które zostaje dla człowieka, brzmi już inaczej: czy zapisane twierdzenie mówi dokładnie to, o co pytał oryginalny problem.

Środowisko zareagowało szybko i po swojemu. Dwa dni po ogłoszeniu matematyk Francesco Fournier-Facio opublikował w serwisie arXiv, gdzie naukowcy udostępniają prace jeszcze przed recenzją, własny tekst. Wziął kryterium techniczne z pracy OpenAI i zbudował na nim mocniejsze przykłady. Metoda nadaje się więc do dalszej pracy, a nie tylko do komunikatu prasowego.

Czego OpenAI nie mówi

Teraz druga strona, bo ogłoszenie ma poważne dziury.

Nie wiadomo, ile było prób nieudanych. Praca ma 249 stron i ani jedna nie opisuje, jak model pracował, jakie dostał polecenia, ile podejść wykonał i gdzie ingerowali ludzie. Jeśli model puszczono na setki otwartych problemów, a pokazano dziesięć, to informacja o pozostałych mówiłaby o jego granicach równie dużo. Gary Marcus zarzuca OpenAI wprost brak punktu odniesienia: nie wiemy, ile z tego zrobiłyby inne modele ani ilu prób trzeba było.

Kwota jest myląca. OpenAI podaje, że tekst potrzebny do znalezienia rozwiązań kosztowałby około 2000 dolarów po stawkach GPT-5.6 Sol. To suma za wszystkie dziesięć wyników i policzona wyłącznie z udanych podejść. Część mediów przepisała to jako 2000 dolarów za jeden problem. Do rachunku nie wchodzi też praca matematyków, którzy przygotowali teksty prac.

Podział pracy opisano jednym zdaniem. Model wygenerował argumenty, ludzie z pomocą tego samego modelu przygotowali z nich prace, a model zapisał je w Lean. Gdzie dokładnie kończył się człowiek, a zaczynała maszyna, nie wiadomo.

I zarzut najmocniejszy. Matematyk Levent Alpoge napisał, że w dobę powtórzył połowę wyników przy użyciu Claude Fable, czyli modelu dostępnego dla każdego, w pełni samodzielnie, przy ogólnie sformułowanym poleceniu i bez dostępu do internetu. Jeśli to się potwierdzi, wyjątkowy nie jest jeden zamknięty model jednej firmy, tylko poziom, na którym są dziś modele w ogóle. Warto dodać, że do kontrprzykładu obalającego hipotezę Connesa równolegle i niezależnie doszedł matematyk Shuoxing Zhou, korzystając ze zwykłego, dostępnego w sprzedaży GPT-5.6 Sol.

Zastrzeżenia dotyczą też formy. Henry Yuen z Columbia University, którego własny dorobek dotyczy jednego z rozwiązanych problemów, chwali wynik, ale krytykuje sposób zapisania dowodu, charakterystyczny jego zdaniem dla tekstów generowanych przez ChatGPT.

Co z tego wynika dla Ciebie

Astry nie kupisz i nie odpalisz. To model wewnętrzny, bez otwartych wag, bez ceny i bez daty premiery, więc na razie jest to zapowiedź, a nie narzędzie.

Zostają dwie rzeczy praktyczne. Pierwsza to wzorzec weryfikacji. Model, który nie tylko twierdzi, ale dostarcza dowód sprawdzalny automatycznie, pokazuje jedyne znane wyjście z problemu, który zna każdy budujący z AI: błędnej odpowiedzi podanej z pełnym przekonaniem. W matematyce takim sprawdzianem jest weryfikator, a w kodzie najbliższym odpowiednikiem są testy. Mechanizm jest ten sam: nie ufaj deklaracji, sprawdź wynik czymś, co nie zależy od modelu.

Druga to dystans do liczb z materiałów producenta. Ta sama zasada, którą stosowaliśmy przy benchmarkach GPT-5.6, obowiązuje i tutaj. Dowody można sprawdzić, więc są mocnym argumentem. Wszystko wokół nich, czyli koszt, samodzielność modelu i skuteczność, znamy wyłącznie z wersji OpenAI.