Ogłoszenia o sztucznej inteligencji, która produkuje dowody matematyczne, przywykliśmy traktować jak deklaracje. Firma mówi, że jej model coś udowodnił, a reszta świata może wierzyć albo nie. Tym razem jest inaczej i to jest w tej sprawie najciekawsze. OpenAI wyłożyło na GitHubie formalizacje wyników w języku Lean 4, na licencji Apache. To znaczy, że dowody może przepuścić przez maszynę każdy, kto zechce. Warto tylko wiedzieć, co taki certyfikat rozstrzyga, a czego nie rozstrzyga wcale.
Co dokładnie leży w repozytorium
Repozytorium nazywa się ten-proofs i zawiera po jednym pliku Lean na każdy z dziesięciu wyników.
Lista jest szeroka i sięga kilku odległych działów. Są tam upakowanie sfer w wysokich wymiarach, kody binarne i sferyczne, grupy niesoficzne oraz hipoteza sztywności Connesa. Dalej złożoność obwodów arytmetycznych, kwantowe powtórzenie równoległe, problem najbliższego wektora, hipoteza objętości Ehrharta, wielokolorowe liczby Ramseya i hipotezy o liczbach ekstremalnych. Według OpenAI każdy z tych problemów pozostawał otwarty co najmniej dekadę.
Jedna rzecz w opisie repozytorium zwraca uwagę przez swoją nieobecność. Plik README nie określa, czy poszczególne wyniki są sformalizowane w całości, czy częściowo. Nie znaczy to, że któryś jest niepełny. Sam plik README tego nie rozstrzyga, a przy dziesięciu wynikach z różnych działów to informacja, której chciałoby się mieć więcej.
Lean sprawdza dowód, nie wybór twierdzenia
Tu leży rozróżnienie, bez którego cała reszta rozmowy się rozjeżdża.
Lean to język, w którym twierdzenie i jego dowód zapisuje się tak formalnie, że program potrafi krok po kroku sprawdzić poprawność rozumowania. Jeśli dowód przechodzi, Lean potwierdza, że sformalizowane twierdzenie wynika z przyjętych aksjomatów. Maszyna nie da się przy tym zagadać, bo nie ocenia stylu ani pewności siebie autora.
Certyfikat nie odpowiada natomiast na drugie pytanie, równie ważne. Nie mówi, czy sformalizowano to twierdzenie, które chciało się udowodnić. Definicję można zapisać nieco inaczej, założenie dołożyć odrobinę mocniejsze, a maszyna i tak potwierdzi poprawność, bo sprawdza to, co dostała. Ocena, czy formalny zapis oddaje pierwotny problem, wraca do człowieka. Dlatego dowody matematyczne przepuszczone przez maszynę są tu mocnym argumentem, ale sprawy nie zamykają.
Czego w tym ogłoszeniu nie ma
Reszta materiału stoi na słowie firmy i warto to nazwać wprost.
Wyniki potwierdził wewnętrznie Sebastien Bubeck, szef badań matematycznych OpenAI. Na razie nie ma informacji o niezależnej recenzji spoza firmy. The Next Web zauważa przy tym, że dopiero się okaże, czy środowisko zaakceptuje dowody matematyczne ogłoszone wpisem na blogu zamiast w recenzowanym czasopiśmie. Thomas Bloom nazwał sprawę dużą wiadomością, co jest reakcją, nie recenzją. Od firmy pochodzą też liczby: manuskrypt na 249 stron i około 2000 dolarów kosztu przebiegów po cenach API. Kwota nie obejmuje ani trenowania modelu, ani pracy ludzi, którzy spisali argumenty.
Jest wreszcie rzecz, która przesądza o możliwości sprawdzenia całości. Astra to kolejna rodzina modeli OpenAI i pozostaje nieudostępniona, bez podanego terminu premiery. Tych przebiegów nie da się więc obecnie niezależnie powtórzyć. Sprawdzić da się formalizację, ale nie przebieg pracy modelu. Podobnie było przy obniżeniu kosztu ataku na schemat kryptograficzny przez badaczy Anthropic, gdzie sprawdzalny był efekt, a nie przebieg pracy modelu.
Pierwsza Misja AI · Kodożercy
Używasz AI codziennie, ale czy robisz to dobrze?
Kurs Pierwsza Misja AI pokaże Ci techniki promptowania, które naprawdę działają. Praktyczne ćwiczenia, gamifikacja i certyfikat na koniec.
Sprawdź program kursu →
Deklaracja lejdejska powstała wcześniej
W czerwcu 2026 ogłoszono deklarację lejdejską, firmowaną przez Międzynarodową Unię Matematyczną. Dokument ostrzega przed skutkami sztucznej inteligencji dla wiarygodności i niezależnej sprawdzalności dowodów oraz dla przypisywania autorstwa. Wśród sygnatariuszy są Kevin Buzzard, Peter Scholze i Leslie Ann Goldberg, a według relacji w ciągu doby podpisało go ponad tysiąc osób. Deklaracja powstała po warsztatach w Lorentz Center jesienią 2025, więc nie jest reakcją na sierpniowy komunikat.
Nie jest też manifestem przeciw sztucznej inteligencji i to warto podkreślić, bo w streszczeniach łatwo o taki skrót. Dokument nie wzywa do zakazu. Postuluje ujawnianie użycia AI w pracy badawczej i utrzymanie rygorystycznej recenzji.
Podsumowanie
OpenAI podaje, że wewnętrzna wersja modelu Astra dała wyniki dla dziesięciu problemów otwartych od co najmniej dekady, między innymi w upakowaniu sfer, hipotezie sztywności Connesa i wielokolorowych liczbach Ramseya. Formalizacje w Lean 4 leżą publicznie na GitHubie na licencji Apache, więc może je sprawdzić maszynowo każdy. Certyfikat potwierdza jednak wyłącznie, że sformalizowane twierdzenie wynika z przyjętych aksjomatów. Nie rozstrzyga, czy sformalizowano właśnie to twierdzenie, o które chodziło. O niezależnej recenzji spoza OpenAI na razie nie ma informacji, potwierdzenie było wewnętrzne, a sam model pozostaje nieudostępniony, więc tych przebiegów nie da się obecnie niezależnie powtórzyć. Dwa miesiące wcześniej Międzynarodowa Unia Matematyczna firmowała deklarację lejdejską, która o taką właśnie sprawdzalność i rzetelną recenzję się upomina.
Newsletter · DevstockAcademy & Kodożercy
Bądź na bieżąco ze światem IT, AI i automatyzacji
Co wtorek: newsy z branży, praktyczne tipy i narzędzia które warto znać. Zero spamu.
