OpenAI publikuje dowód dla problemu Naviera–Stokesa. Co naprawdę sprawdził Lean?

OpenAI opublikowało analityczny dowód i formalizację w Lean, które według firmy rozwiązują problem istnienia i gładkości Naviera–Stokesa przez wykazanie osobliwości w skończonym czasie. To potencjalnie historyczny wynik, ale 9 września 2026 r. nie jest jeszcze rozstrzygnięciem uznanym przez Clay Mathematics Institute. Najważniejsze pytanie brzmi dziś nie „czy plik Lean się sprawdza”, lecz czy zakodowane w nim twierdzenie dokładnie odpowiada problemowi i przejdzie niezależną ocenę matematyków.

Najważniejsze fakty

• OpenAI udostępniło 8 września komunikat, tekst dowodu i formalizację Lean.
• Firma twierdzi, że konstrukcja ustanawia warianty C i D oficjalnego problemu: płyn zaczyna w spoczynku, działa na niego gładka siła zewnętrzna, energia pozostaje skończona, ale prędkość staje się nieograniczona w skończonym czasie.
• Według OpenAI około 10 tys. agentów pracowało nad problemem przez około 88 godzin, a formalizacja miała zająć kolejne 17 godzin.
• Lean zwiększa wiarygodność kontroli logicznej, ale nie zastępuje sprawdzenia, czy formalny zapis wiernie odpowiada problemowi Clay.
• Nie przyznano nagrody ani oficjalnie nie zamknięto problemu. Reguły Clay przewidują publikację w kwalifikowanym źródle, minimum dwa lata oceny i powszechną akceptację środowiska.

Co dokładnie ogłosiło OpenAI?

W 166-stronicowym preprincie „Finite Time Blowup for Navier–Stokes” OpenAI konstruuje rozwiązanie trójwymiarowych równań nieściśliwego płynu dla dowolnej dodatniej lepkości. Przepływ ma zerową prędkość początkową, a gładka siła jest ograniczona do skończonego obszaru przestrzeni i czasu. Mimo to maksymalna prędkość ma rosnąć bez ograniczeń, gdy czas zbliża się do chwili powstania osobliwości, podczas gdy całkowita energia kinetyczna pozostaje ograniczona.

To precyzyjny i ważny zakres. Nie chodzi o „wzór rozwiązujący każdy przepływ”, prognozę turbulencji ani awarię praw fizyki. Chodzi o matematyczną konstrukcję pokazującą, że idealizowany model ciągłego płynu może utracić gładkość nawet przy dodatniej lepkości i dobrze zachowującej się sile zewnętrznej.

OpenAI wiąże wynik z wariantami C i D oficjalnego sformułowania Clay Mathematics Institute. Wariant C dotyczy całej przestrzeni R³, a D wersji okresowej, matematycznie reprezentowanej przez trójwymiarowy torus. W obu przypadkach dopuszczona jest gładka siła zewnętrzna. To istotne, bo często powtarzana w skrótach wersja problemu — czy gładki przepływ bez wymuszenia zawsze pozostaje gładki — odpowiada innym wariantom oficjalnego zadania.

Dlaczego osobliwość ma znaczenie?

Równania Naviera–Stokesa opisują ruch cieczy i gazów jako ośrodka ciągłego. Wykorzystuje się je w aerodynamice, prognozowaniu pogody czy modelowaniu przepływu krwi. W trzech wymiarach nie było wiadomo, czy gładki stan początkowy może w skończonym czasie doprowadzić do punktu, w którym prędkość staje się matematycznie nieograniczona.

Proponowana konstrukcja OpenAI ma postać kurczącego się wiru. Jego rdzeń zwęża się i wydłuża, a ruch obrotowy przyspiesza. Klucz polega na takim zbilansowaniu przyspieszenia, ciśnienia, transportu pędu i lepkości, aby ich ogromne składowe wzajemnie się znosiły. Pozostała siła zewnętrzna nadal ma być gładka, choć sama prędkość dąży do nieskończoności.

Nie wynika z tego, że samoloty, oceany albo naczynia krwionośne nagle osiągną nieskończoną prędkość. Model ciągły przestaje mieć sens, zanim dotrzemy do skali pojedynczych cząsteczek. Znaczenie wyniku jest przede wszystkim matematyczne: pokazywałby granicę jednego z podstawowych modeli mechaniki płynów.

Co sprawdził Lean — i czego nie sprawdził?

Lean jest asystentem dowodzenia. Matematyk lub system AI zapisuje definicje, założenia i kolejne kroki w formalnym języku, a niewielkie jądro programu sprawdza, czy każdy wniosek rzeczywiście wynika z wcześniejszych reguł. Daje to znacznie mocniejszą ochronę przed przeoczonym rachunkiem lub ukrytą luką niż zwykły, narracyjny zapis na papierze.

Formalizacja nie jest jednak automatycznym stemplem „Problem Milenijny rozwiązany”. Jak zwraca uwagę Quanta Magazine, ludzie muszą jeszcze sprawdzić, czy twierdzenie udowodnione w Lean jest logicznie równoważne temu, co matematycy zamierzali wykazać. Audytu wymagają definicje, zależności od bibliotek, tłumaczenie analizy na formalny zapis i zgodność z warunkami Clay.

Innymi słowy: poprawne przejście formalnej kontroli oznacza, że dowód działa w opisanym systemie założeń. Nie oznacza samo przez się, że właściwie zakodowano każdy niuans oryginalnego problemu. To szczególnie ważne przy 166 stronach analizy i bardzo rozbudowanym certyfikacie formalnym.

Jak AI znalazła dowód?

Według OpenAI prace rozpoczęły się 1 września. Firma użyła wewnętrznego modelu, który określa jako znacząco bardziej zdolny od GPT‑6 Astra, oraz systemu grup komunikujących się agentów. Około 10 tys. agentów miało pracować nad wariantami problemu równolegle przez 88 godzin. Sam etap Naviera–Stokesa wygenerował według firmy 2,7 mln wiadomości i około 130 mld tokenów wyjściowych.

Po odkryciu argumentu GPT‑6 Astra miała w dodatkowe 17 godzin przeprowadzić formalizację i weryfikację w Lean. Te liczby pochodzą wyłącznie od producenta; nie ma publicznego audytu kosztu obliczeń. Model, który znalazł dowód, nie jest dostępny w aplikacji ani API, nie ma też opublikowanej specyfikacji lub cennika.

Skala tego eksperymentu pokazuje nowy typ badań: zamiast jednego modelu odpowiadającego na jeden prompt tysiące instancji przeszukują różne kierunki, przekazują sobie wyniki i konsolidują obiecujące idee. To rozwinięcie nurtu modeli rozumujących, w którym pracują także badacze tacy jak Szymon Sidor. Zarazem ogromna liczba agentów utrudnia odtworzenie procesu i ocenę, które pomysły były naprawdę decydujące.

Co z pracami Buckmastera i Alpögego?

Ogłoszenie OpenAI zbiegło się z publikacją wyników Tristana Buckmastera z New York University i Leventa Alpögego z Anthropic. Ich prace dotyczą kilku blisko spokrewnionych równań, w tym wymuszonego równania Eulera. Euler opisuje przepływ bez lepkości, więc sam nie jest problemem Naviera–Stokesa z listy Clay.

OpenAI uznaje pierwszeństwo Buckmastera i Alpögego dla wymuszonego Eulera, a własny wynik Eulera opisuje jako wariant bez wymuszenia. Obie linie badań wykorzystują wcześniejsze idee Diego Córdoby i Luisa Martíneza-Zoroi: kaskadę coraz mniejszych struktur wirowych, które wzmacniają przepływ. Niezależne omówienia w Quanta i Nature podkreślają zarówno wagę wcześniejszych prac, jak i konieczność spokojnego ustalenia chronologii oraz znaczenia nowych dowodów.

Spór o pierwszeństwo i przepływ informacji nie powinien przesłaniać matematycznej różnicy między równaniami, założeniami o wymuszeniu i dokładnym typem osobliwości. Na obecnym etapie nie ma podstaw, by utożsamiać wszystkie ogłoszone wyniki albo rozstrzygać zarzuty na podstawie publicznych relacji stron.

Czy Problem Milenijny jest już rozwiązany?

Najuczciwsza odpowiedź brzmi: OpenAI opublikowało bardzo poważną propozycję rozwiązania i formalny certyfikat, ale procedura uznania dopiero się zaczyna. Pierwsze wypowiedzi uznanych matematyków są pozytywne. Quanta przytacza Charlesa Feffermana, autora oficjalnego opisu problemu Clay, a Nature — Martina Bridsona, prezesa instytutu. To ważne sygnały, lecz nie formalna decyzja.

Reguły Clay Mathematics Institute są celowo powolne. Proponowane rozwiązanie musi ukazać się w kwalifikowanym źródle, od publikacji muszą minąć co najmniej dwa lata, a wynik musi zdobyć powszechną akceptację międzynarodowego środowiska matematycznego. Dopiero wtedy CMI może podjąć szczegółową ocenę. Instytut nie przyjmuje bezpośrednich zgłoszeń, a OpenAI deklaruje, że nie zamierza ubiegać się o nagrodę na podstawie samego komunikatu.

Historia matematyki zna wyniki, których sprawdzanie zajmowało lata. Formalizacja może ten proces przyspieszyć, bo zawęża przestrzeń możliwych błędów, ale nie usuwa potrzeby recenzji. Podobnie jak w klasycznej analizie funkcjonalnej, której fundamenty przybliża nasz tekst o Stefanie Banachu, definicje i zakres twierdzenia są równie ważne jak sam ciąg przekształceń.

Co warto obserwować dalej?

Najważniejsze będą trzy rzeczy. Po pierwsze, niezależni specjaliści muszą zmapować formalizację Lean na warianty C i D oraz sprawdzić jej zależności. Po drugie, matematycy ocenią analityczny argument: czy wszystkie regularności, granice i własności siły zewnętrznej są dokładnie takie, jak wymaga oficjalne zadanie. Po trzecie, trzeba ustalić miejsce publikacji i rozpocząć właściwy proces recenzji.

Nawet jeśli w dowodzie pojawi się luka, skala pracy agentowej i możliwość przełożenia tak długiego argumentu na Lean pozostaną ważnym sygnałem dla nauki wspomaganej przez AI. Jeśli natomiast wynik wytrzyma kontrolę, będzie to przełom podwójny: w analizie równań różniczkowych i w sposobie organizowania badań przez systemy sztucznej inteligencji.

Dziś właściwy nagłówek nie brzmi więc „AI definitywnie rozwiązała Naviera–Stokesa”, lecz: OpenAI udostępniło kandydacki dowód o wyjątkowej wadze, wraz z formalizacją umożliwiającą precyzyjny audyt. Matematyka dostała materiał do sprawdzenia — werdykt dopiero nadejdzie.