1 sierpnia 2026 roku OpenAI poinformowało, że wewnętrzna wersja jego kolejnego modelu, nazwana Astra, przedstawiła nowe wyniki dotyczące dziesięciu otwartych problemów matematyki i informatyki teoretycznej. Każdy z nich pozostawał nierozwiązany od co najmniej dziesięciu lat. Astra nie jest modelem publicznym: nikt poza OpenAI nie może jej uruchomić.
To ostatnie zdanie pojawia się zwykle na końcu relacji o Astrze, jeśli w ogóle. Tymczasem to ono decyduje o tym, jak należy czytać całą resztę. Poniżej nie chodzi o to, czy sztuczna inteligencja „robi matematykę”. Chodzi o pytanie węższe i znacznie bardziej użyteczne: skąd właściwie wiemy, że te wyniki są poprawne, i w którym dokładnie miejscu ta wiedza się kończy.
Co zostało opublikowane
Materiał towarzyszący ogłoszeniu składa się z trzech elementów. Po pierwsze, manuskrypt liczący 249 stron. Po drugie, ślady rozumowania modelu, czyli zapis drogi, którą przeszedł. Po trzecie, i to jest część najważniejsza, certyfikaty dowodowe w Lean 4, sprawdzalne maszynowo. Całość trafiła na GitHuba na licencji Apache 2.0.
Sposób udostępnienia jest tu istotniejszy niż zwykle. Komunikat prasowy, zrzut ekranu z rozmowy albo artykuł opisujący wynik wymagają zaufania do autora. Repozytorium z formalnymi dowodami wymaga wyłącznie tego, żeby ktoś je pobrał i uruchomił. Różnica między tymi dwoma sytuacjami jest większa niż różnica między dziesięcioma a dwudziestoma rozwiązanymi problemami.
Lean 4 to asystent dowodzenia: język, w którym twierdzenie i jego dowód zapisuje się na tyle formalnie, że program potrafi skontrolować każdy pojedynczy krok wnioskowania. Kompilator albo dowód przyjmuje, albo go odrzuca. Nie ma stanu pośredniego i nie ma kategorii „wygląda przekonująco”.
Co znaczy licznik sorry ustawiony na zero
W Lean istnieje słowo kluczowe sorry. Wstawia się je w miejsce kroku, którego jeszcze nie udowodniono, żeby reszta pliku dała się skompilować mimo luki. Jest to więc jawnie oznaczony dług: tutaj brakuje argumentu, wrócę do tego później. Praktyka jest powszechna i całkowicie uczciwa, pod warunkiem że dług zostanie w końcu spłacony.
Repozytorium z certyfikatami Astry pokazuje licznik sorry ustawiony na zero. W praktyce oznacza to, że w formalizacji nie ma ani jednego kroku pozostawionego w zawieszeniu, ani jednego miejsca, w którym autor prosiłby czytelnika o zaufanie. To konkretna, mierzalna właściwość opublikowanego kodu, a nie deklaracja: każdy może pobrać repozytorium, uruchomić kompilację u siebie i sam policzyć.
Czego dotyczą wyniki
Dziesięć problemów rozkłada się na kilka odległych od siebie dziedzin: teoria grup, algebry von Neumanna, geometria w dużych wymiarach, złożoność kwantowa, kryptografia oparta na kratach euklidesowych oraz kombinatoryka ekstremalna.
Wynikiem wymienianym najczęściej jest pierwsza jawna konstrukcja grupy niesoficznej. Pojęcie soficzności wprowadził Michaił Gromow w 1999 roku, a pytanie o istnienie grupy niesoficznej pozostawało od tamtej pory jednym z centralnych otwartych pytań teorii grup. Astra miała też rozwiązać trzy problemy związane z Paulem Erdősem.
Thomas Bloom, matematyk z Uniwersytetu w Manchesterze, który prowadzi katalog problemów Erdősa, określił te wyniki na platformie X jako „big news”. Warto zwrócić uwagę, kto to mówi: osoba, która zawodowo prowadzi katalog problemów Erdősa, a trzy z dziesięciu wyników dotyczą właśnie tych problemów.
Dlaczego Lean zmienia charakter twierdzenia
Podstawowy zarzut wobec modeli językowych w matematyce brzmi: halucynacje. Model generuje tekst, który ma strukturę dowodu, używa właściwego słownictwa, przechodzi od przesłanek do wniosku i bywa przy tym po prostu błędny. Wyłapanie takiego błędu spada na recenzenta. Przy argumencie rozłożonym na kilkadziesiąt stron to praca na tygodnie, w dodatku praca zawodna, bo człowiek czytający formalnie poprawnie brzmiący tekst ma skłonność do przeoczeń.
Format Lean odpowiada na ten zarzut wprost. Poprawność dowodu przestaje być kwestią oceny czytelnika i staje się właściwością sprawdzalną programowo. Twierdzenie, które przeszło przez weryfikator mechaniczny, ma inny status niż zdanie wygenerowane przez model językowy. Nie chodzi o to, że jest „bardziej prawdopodobnie prawdziwe”. Chodzi o to, że sposób ustalania jego prawdziwości jest inny.
To rozróżnienie ma zastosowanie daleko poza matematyką. Kiedy system generatywny wypuszcza jakikolwiek artefakt, pytanie kluczowe brzmi: czy istnieje niezależny mechanizm zdolny ten artefakt odrzucić? Jeśli tak, ufamy mechanizmowi, a nie modelowi, i jakość modelu przestaje być głównym źródłem ryzyka. Jeśli nie, ufamy modelowi, co jest zupełnie inną sytuacją, nawet jeśli wygląda podobnie.
Jak sprawdzić to samodzielnie
Ta droga nie wymaga bycia matematykiem, wymaga tylko środowiska Lean. Pobiera się repozytorium, uruchamia kompilację certyfikatów, sprawdza, czy przechodzi bez błędów, i weryfikuje, że w plikach nie ma wystąpień sorry. Po tej operacji wiadomo, że dowody trzymają się w Lean. Trudniejsza część zaczyna się dopiero potem i wymaga przeczytania samych sformułowań twierdzeń, o czym niżej.
Granica, o której prawie się nie pisze
Tutaj kończy się większość relacji na ten temat, i jest to niefortunne, bo w tym właśnie miejscu zaczyna się najciekawsza część sprawy.
Udana kompilacja w Lean potwierdza, że dowód jest poprawny dla twierdzenia w takiej postaci, w jakiej zostało zapisane w Lean. Nie potwierdza automatycznie, że ten formalny zapis oddaje otwarty problem tak, jak rozumiała go społeczność matematyczna.
Między jednym a drugim jest krok, którego żaden kompilator nie wykona: przekład z matematyki pisanej językiem naturalnym na formalną definicję. Ten przekład wykonuje człowiek albo model, i to on jest miejscem, przez które może wejść błąd. Definicja bywa subtelnie węższa od oryginalnego pytania. Może zawierać dodatkowe założenie, przy którym twierdzenie jest prawdziwe, ale znacznie mniej interesujące. Może opisywać obiekt, który tylko nazywa się tak samo jak ten, o który chodziło.
Weryfikator kontroluje wnioskowanie od aksjomatów do tezy. Nie kontroluje, czy teza jest tą tezą. Ta ocena należy do ludzi, wymaga czasu i na moment publikacji nie została rozstrzygnięta. Uznanie formalnych sformułowań za równoważne otwartym problemom jest dokładnie tym, co pozostaje w zawieszeniu, i nie da się tego przyspieszyć mocą obliczeniową.
Analogia z inżynierią oprogramowania jest bezpośrednia. Przechodzący zestaw testów dowodzi, że kod spełnia specyfikację taką, jak ją zapisano. Nie dowodzi, że specyfikacja opisuje to, czego potrzebował klient. Zielone testy przy błędnym produkcie to sytuacja codzienna w każdym zespole. Lean przesuwa granicę zaufania nieporównanie dalej niż testy jednostkowe, ale jej nie likwiduje: przesuwa ją do sformułowania twierdzenia.
Dwa tysiące dolarów: co mierzy ta liczba
Liczba, która obiegła relacje o Astrze, to około 2 000 dolarów kosztu obliczeń. Brzmi jak informacja o tym, ile kosztuje dzisiaj rozwiązanie problemu otwartego od dekady. Nie jest to jednak to, co ta liczba mierzy.
Badacze zwracają uwagę, że kwota obejmuje przebiegi udane, a nie wszystkie próby modelu. Jest to zatem koszt publikacji, nie koszt odkrycia. Ile obliczeń pochłonęły ścieżki, które donikąd nie doprowadziły, nie zostało podane. Bez tego mianownika liczba 2 000 dolarów nie mówi nic o efektywności procesu, mówi wyłącznie o cenie przebiegów zakończonych sukcesem.
Zastrzeżenie to łączy się z drugim, dotyczącym selekcji. To OpenAI zdecydowało, które wyniki opublikować. Nie wiadomo, ile prób zakończyło się formalizacją, która się nie skompilowała, ani ile hipotez okazało się fałszywych, ani ilu problemów model w ogóle nie ruszył. Dziesięć opublikowanych wyników to licznik ułamka, którego mianownika nie znamy. Nie jest to zarzut nieuczciwości, tylko opis tego, czego z takiej publikacji wywnioskować nie można.
Sprawdzalne to nie to samo co odtwarzalne
Trzecie zastrzeżenie dotyczy niezależnej weryfikacji i jest najsubtelniejsze, bo opiera się na rozróżnieniu dwóch słów, które w potocznym użyciu bywają wymienne.
Badacze spoza OpenAI zwracają uwagę, że pracownicy firmy pomagali przygotować artykuły i sformalizować argumenty. Nikt poza firmą nie może uruchomić modelu, który wykonał pracę. W konsekwencji wynik daje się zweryfikować, ale nie daje się odtworzyć.
Różnica jest zasadnicza. Weryfikacja oznacza: pobieram opublikowane certyfikaty, kompiluję je i potwierdzam, że dowód się trzyma. To może zrobić każdy i na tym polega realna wartość tej publikacji. Odtworzenie oznaczałoby: biorę model, zadaję mu jedenasty problem otwarty i sprawdzam, czy powstaje porównywalny wynik. Tego nie może zrobić nikt z zewnątrz.
Twierdzenia zawarte w pracy są więc mocne w tej postaci, w jakiej zostały zapisane w Lean. Twierdzenie o zdolnościach modelu, który je wygenerował, pozostaje twierdzeniem OpenAI, popartym artefaktami, lecz nie sprawdzonym niezależnie. Gary Marcus zauważa przy tym, że niezależnie od tego, jak wyniki są imponujące, nie dowodzą one istnienia ogólnej sztucznej inteligencji ani nadejścia uniwersalnego solvera.
Co z tego wynika dla osoby prowadzącej firmę
Bezpośrednio: niewiele. Grupy niesoficzne nie wpłyną na Państwa plan produktowy. Pośrednio są tu jednak trzy rzeczy warte zapamiętania i żadna z nich nie wymaga ekstrapolacji.
Po pierwsze, weryfikowalność jest decyzją projektową, a nie właściwością modelu. Wynik Astry jest wiarygodny dlatego, że został wypuszczony w formacie, który maszyna potrafi odrzucić. Ta sama zasada obowiązuje w każdym zastosowaniu generatywnym w firmie. Jeżeli model pisze kod, weryfikatorem są testy, typy i lintery. Jeżeli uzupełnia dane, weryfikatorem jest walidacja schematu. Jeżeli produkuje treść, której nikt nie sprawdza mechanicznie, przyjmują Państwo ryzyko rosnące proporcjonalnie do objętości produkcji.
Po drugie, warto pytać o mianownik. Każda demonstracja pokazuje przebiegi udane. Pytanie brzmi zawsze: ile było wszystkich. Przy wyborze narzędzia jest to jedyna liczba pozwalająca oszacować rzeczywisty koszt jednostkowy, i zwykle jest to liczba, której dostawca nie podaje sam z siebie.
Po trzecie, luka między sformułowaniem a intencją nie znika. Automatyzacja ją przesuwa, nigdy nie zamyka. Kompilator Lean nie oceni, czy definicja opisuje właściwy obiekt, dokładnie tak samo, jak potok CI nie oceni, czy funkcja rozwiązuje właściwy problem biznesowy. Im lepsze narzędzia weryfikacji, tym większa część ryzyka koncentruje się na poprawnym postawieniu pytania. To argument za tym, żeby na specyfikację poświęcać więcej czasu, a nie mniej.
Warto też zachować proporcje, patrząc na to, co działo się w tym samym miesiącu. OpenAI obniżyło cenę GPT-5.6 Luna o 80 procent, do 0,20 dolara za milion tokenów wejściowych. ChatGPT ma około miliarda aktywnych użytkowników tygodniowo. Anthropic akcentuje lepsze wyniki w programowaniu i okno kontekstu rzędu miliona tokenów. Dziesięć dowodów w Lean jest wydarzeniem w matematyce. Na Państwa rachunek za API realny wpływ ma raczej pierwsza z tych informacji.
Wniosek
Ustalone jest to: dziesięć dowodów zostało opublikowanych w formacie sprawdzalnym maszynowo, bez ani jednego sorry, na otwartej licencji, i każdy może je skompilować u siebie. Jest to nieporównanie mocniejsza forma przedstawienia wyniku niż komunikat prasowy albo zrzut ekranu z rozmowy z modelem.
Nieustalone jest to: czy formalne sformułowania odpowiadają problemom otwartym tak, jak rozumiała je społeczność matematyczna; jaki był pełny koszt, licząc próby nieudane; oraz czy model powtórzyłby wynik na jedenastym problemie, ponieważ nikt spoza OpenAI nie może go o to zapytać.
Obie listy są prawdziwe jednocześnie i nie znoszą się nawzajem. Czytelnik, który zapamięta tylko pierwszą, wyciągnie wniosek za mocny. Czytelnik, który zapamięta tylko drugą, przeoczy zmianę realną: format, w którym twierdzenie o wyniku modelu daje się rozstrzygnąć bez zaufania do jego autora, zmienia naturę takiego twierdzenia. Czy formalne sformułowania odpowiadają otwartym problemom, rozstrzygną dopiero matematycy czytający same sformułowania, i na moment publikacji nie jest to przesądzone.
W Go To Agency stosujemy tę samą zasadę do rzeczy dużo prostszych niż teoria grup: jeżeli czegoś nie da się sprawdzić automatycznie, nie uznajemy tego za gotowe. Jeśli chcą Państwo omówić konkretny projekt, pracujemy pisemnie i odpowiadamy w ciągu 24 godzin roboczych.
