OpenAI: model Astra rozwiązał 10 otwartych problemów matematyki

OpenAI poinformowało 1 sierpnia 2026 roku, że jego wewnętrzny model — w relacjach branżowych utożsamiany z wersją systemu Astra — rozwiązał dziesięć od lat otwartych problemów z matematyki i teoretycznej informatyki. Firma opublikowała pełną pracę z dowodami, ich formalizacje w języku Lean 4 oraz koszt obliczeń: poniżej 2000 dolarów (ok. 8 tys. zł) na jeden problem.

Najważniejsze w skrócie

Dziesięć problemów z czystej matematyki i teoretycznej informatyki, każdy bez postępu od co najmniej dekady
Koszt poniżej 2000 USD (ok. 8 tys. zł) na problem, liczony po cenach tokenów GPT-5.6 Sol
Dowody sformalizowane w Lean 4 i opublikowane w repozytorium openai/ten-proofs na GitHubie
Osobny dokument PDF rekonstruuje tok rozumowania, który doprowadził do wyników
Dla porównania wcześniejsze kryptograficzne badanie Anthropic z modelem Claude kosztowało ok. 100 000 USD (ok. 400 tys. zł)

Co rozwiązał model

Praca „Ten Advances in Mathematics and Theoretical Computer Science" zbiera wyniki z dwóch światów. Po stronie czystej matematyki model obalił hipotezę rigidity Connesa, konstruując nieskończenie wiele nieizomorficznych grup o tej samej algebrze von Neumanna, oraz udowodnił ostrą postać hipotezy objętościowej Ehrharta. Wyznaczył też dokładne tempo wykładnicze liniowego programu Cohna-Elkiesa dla upakowania sfer w wysokich wymiarach — problemu, którego zachowanie asymptotyczne pozostawało nieznane.

Po stronie informatyki teoretycznej wyniki dotyczą złożoności obliczeniowej. Model wykazał dolne granice dla obwodów arytmetycznych liczących permanentpermanent: Funkcja macierzy podobna do wyznacznika, ale bez naprzemiennych znaków — jej obliczenie jest wyjątkowo kosztowne., udowodnił wykładnicze twierdzenie o równoległym powtarzaniu dla skończonych gier splątanych oraz uzyskał nowy wynik o trudności problemu najbliższego wektora (CVP) przez redukcję z 3SAT3SAT: Kanoniczny problem NP-zupełny: czy formułę logiczną z klauzulami po trzy zmienne da się spełnić.. Do listy dołączają superwykładnicza dolna granica dla wielokolorowych liczb Ramseya i obalenie dwóch hipotez z ekstremalnej teorii grafów Erdősa i Simonovitsa.

Weryfikowalność, nie tylko deklaracja

Kluczowy element to sposób udostępnienia wyników. Dowody sformalizowano w Lean 4 — języku, w którym poprawność rozumowania sprawdza maszyna, a nie recenzent. To odróżnia ogłoszenie od samych deklaracji o „rozwiązaniu" problemów. OpenAI dołączyło pełną pracę oraz wygenerowany przez model dokument opisujący, jak dochodził do dowodów. Transparentność ma jednak granice — jak zauważa Simon Willison, firma nie ujawniła użytych promptów.

To przyzwoity poziom transparentności, ale chcę zobaczyć prompty, których użyli.

Simon Willison, autor bloga o AI i współtwórca frameworku Datasette.

Koszt jako sygnał

Najbardziej wymowna liczba to nie sama lista problemów, lecz cena. Poniżej 2000 dolarów na problem — przy cenach tokenów GPT-5.6 Sol — plasuje taką pracę w zasięgu pojedynczego laboratorium, a nie tylko wielkiej korporacji. Dla porównania wcześniejsze badanie Anthropic, w którym model Claude znajdował słabości w szyfrach HAWK i AES, kosztowało według relacji ok. 100 000 dolarów. Różnica dwóch rzędów wielkości pokazuje, jak szybko spada koszt maszynowej pracy badawczej.

< 2000 USDkoszt rozwiązania jednego problemu (ceny tokenów GPT-5.6 Sol)OpenAI

Wpisuje się to w wizję „dużej matematyki" (big mathematics) Terence'a Tao — rozproszonej współpracy ludzi i maszyn, w której AI przejmuje techniczną, żmudną część, a ludzie zachowują część twórczą.

Dlaczego to ważne?

Ogłoszenie przesuwa punkt odniesienia dla AI w nauce. Do tej pory modele językowe traktowano głównie jako asystentów — tu wygenerowały nowe, weryfikowalne wyniki na poziomie badawczym, i to tanio. Formalizacja w Lean 4 odbiera najczęstszy zarzut wobec takich zapowiedzi, czyli brak sprawdzalności. Jeśli koszt rzeczywiście spadł do tysięcy dolarów za problem, matematyka i teoretyczna informatyka mogą stać się pierwszymi dziedzinami, w których modele generują oryginalną wiedzę szybciej, niż środowisko zdąży ją zrecenzować. To zmienia pytanie z „czy AI pomaga" na „kto weryfikuje".

Co dalej?

Środowisko matematyczne musi niezależnie zrecenzować dziesięć dowodów — formalizacja Lean 4 przyspiesza ten proces, ale nie zastępuje oceny istotności wyników
OpenAI nie ujawniło promptów ani pełnych szczegółów modelu, co pozostaje otwartą kwestią dla powtarzalności
Spadek kosztu poniżej 2000 USD na problem zapowiada więcej takich prac z innych laboratoriów w kolejnych miesiącach