Czy AI właśnie rozwiązała Naviera–Stokesa? Co faktycznie dowodzi roszczenie OpenAI

OpenAI twierdzi, że jeden z jej wewnętrznych systemów rozgryzł jeden z Millennium Prize Problems Instytutu Claya. To historia wyjątkowa i byłaby jak dotąd największym matematycznym odkryciem wspartym przez AI. Jest jednak też druga opowieść: walka o to, komu naprawdę należą się zasługi.

Oto co faktycznie się wydarzyło: OpenAI usłyszała plotkę, że model konkurencyjnego laboratorium poczynił postępy w jednym z najsłynniejszych nierozwiązanych problemów matematyki. Ta plotka wystarczyła, by uruchomić sprint: aby podjąć problem, OpenAI użyła 10 000 równoległych agentów AI, 88 godzin mocy obliczeniowej i około 22,5 mln dol. skumulowanych kosztów. Teraz firma twierdzi, że ma prawdziwy dowód. A co z nagrodą 1 mln dol.? OpenAI mówi, że nie zamierza jej odebrać. (Może po prostu nie potrzebują pieniędzy.)

Krótka odpowiedź: Nagroda 1 mln dol. Claya za Naviera–Stokesa nie została zdobyta. To, co OpenAI twierdzi, że dowiodła, dotyczy konkretnego wariantu problemu — wybuchowości pod gładkim wymuszeniem — który pozostaje niezweryfikowany przez niezależnych matematyków. To, czy spełnia pełny problem w rozumieniu większości ekspertów, jest realnie kwestionowane.

Czym jest równanie Naviera–Stokesa i dlaczego jest warte 1 mln dol.?

Aby zrozumieć, co twierdzi OpenAI, musisz najpierw wiedzieć, co sprawia, że Navier–Stokes jest tak trudny.

Równania Naviera–Stokesa opisują ruch płynów: wody, powietrza, krwi. Leżą u podstaw prognoz pogody, projektowania samolotów i medycyny krążenia. Sformułowane w XIX wieku, w praktyce działają znakomicie. Pytanie matematyczne brzmi, czy działają zawsze: czy gładkie, dobrze zachowujące się rozwiązania istnieją zawsze, czy też płyn rządzony tymi równaniami może w skończonym czasie rozwinąć osobliwość — punkt, w którym prędkość staje się nieskończona?

To pytanie, znane jako problem „istnienia i gładkości”, jest jednym z siedmiu Millennium Prize Problems Instytutu Matematycznego Claya, z których każdy opatrzono nagrodą 1 mln dol. Do dziś rozwiązano tylko jeden z tych problemów: hipotezę Poincarégo, w 2003 roku.

Dlaczego ten problem nas obchodzi: Czasem problemy matematyczne są w dużej mierze czysto akademickie. Ten jednak nie jest tylko abstrakcyjną łamigłówką. Każdy model pogodowy, każda symulacja lotu i każde narzędzie inżynieryjne oparte na tych równaniach milcząco zakłada, że zachowują się one „grzecznie”, ale nikt nie dowiódł, że to założenie zawsze jest prawdziwe. Gdyby okazało się, że rozwiązania mogą eksplodować w skończonym czasie, ujawniłoby to realną lukę między matematyką, na której polegamy, a systemami fizycznymi, które ma opisywać.

Co tak naprawdę OpenAI twierdzi, że dowiodła

Historia zaczyna się nie od wglądu matematycznego, lecz od plotki. Sam Altman przyznał, że OpenAI rozpoczęła wysiłek po tym, jak usłyszała, że modele Anthropic rozwiązały duży problem matematyczny, pisząc na X: „Byliśmy ciekawi, czy nasze też potrafią”.

Tygodniowy sprint objął wiele problemów z listy Millennium Prize i zużył łącznie 300 miliardów tokenów wyjściowych, co oznacza około 22,5 mln dol. mocy obliczeniowej we wszystkim, co próbowano. Sam problem Naviera–Stokesa pochłonął około 130 miliardów tych tokenów i 2,7 miliona wiadomości. Dziesięć tysięcy agentów pracowało równolegle od 1 do 6 września. A potem — tu powinna zapalić ci się lampka — OpenAI oznajmiła, że nie zamierza ubiegać się o nagrodę 1 mln dol., przedstawiając wynik jako dowód na to, jak szybko postępują jej modele.

Zanim dotarły do Naviera–Stokesa, agentki OpenAI najpierw rozwiązały problem regularności niezmuszonych równań Eulera, używając prawie 100 agentów w około 50 godzin. Ustalając najpierw zachowanie wybuchowe w prostszym układzie Eulera, agenci zbudowali konceptualne podstawy, które uczyniły podejście do Naviera–Stokesa wykonalnym.

Tu właśnie liczy się drobny druk. Oficjalna formulacja Claya dla Naviera–Stokesa obejmuje cztery opcje, oznaczone A, B, C i D. Opcje A i B pytają o globalnie gładkie rozwiązania bez wymuszenia zewnętrznego — w zwykłej przestrzeni trójwymiarowej lub w domenie okresowej. Opcje C i D dopuszczają przykłady wybuchu z gładkim członem wymuszającym. Dowód OpenAI celuje w opcje C i D, co oznacza, że wariant z wymuszeniem jest rzeczywiście częścią oficjalnego problemu Claya.

To powiedziawszy, wielu matematyków uważa opcje A i B za głębsze pytanie, ponieważ wymuszenie jest nałożone z zewnątrz: wybierasz siłę, by spowodować wybuch, zamiast pytać, czy równania potrafią załamać się same z siebie. Czy podejście da się rozszerzyć tak, by usunąć wymuszenie i zmierzyć się z A i B — na razie nie wiadomo, i to pytanie pozostaje zdecydowanie otwarte. Różnica między tym, co pokazano, a tym, co wielu ekspertów uważa za sedno problemu, to właściwy wniosek.

Kulisy sporu o to, komu należą się zasługi

Skoro już wiemy, co faktycznie udowodniono, ludzka strona historii ma wyraźny wątek przewodni — jeśli odejdziemy od przepychanek słownych.

15 sierpnia Tristan Buckmaster i Levent Alpöge z Anthropic dowiedli, że równania Eulera, bez-tarciowy kuzyn Naviera–Stokesa, mogą eksplodować pod gładkim wymuszeniem, rozwijając podejście Diego Córdoby i Luisa Martíneza-Zoroi. Ich wyniki obejmowały też równania Boussinesqa oraz nieściśliwego przepływu w ośrodku porowatym. Prace trwały około roku. Były nieopublikowane, w toku, budowane po cichu. Potem słowo się rozeszło.

Sprint OpenAI zaczął się 1 września po usłyszeniu plotki, którą później powiązano z Alpöge i Buckmasterem. Buckmaster wysłał prywatnego maila do OpenAI 3 września, gdy dowiedział się, że jego praca trafiła do firmy. Po zakończeniu projektu i weryfikacji w Lean 6 września OpenAI skontaktowała się, by zaproponować równoczesną publikację. Wersja Buckmastera co do tego, co nastąpiło później, jest znacznie ostrzejsza: opisuje on rozmowy, w których — jak twierdzi — naciskano go w sprawie publikacji i autorstwa, łącznie z sugestiami wykluczenia Alpöge ze względu na jego zatrudnienie w Anthropic.

Buckmaster utrzymuje, że gdy zasygnalizował zamiar upublicznienia tych obaw, usłyszał: „Dlaczego miałbyś niszczyć swoją karierę?” oraz „Jeśli nie chcesz, żebym był miły, to nie muszę być miły.” Bubeck nazwał te zarzuty „fałszywymi i podsycającymi emocje”. OpenAI zaprzecza, by uzyskała dostęp do jakichkolwiek prywatnych promptów czy nieopublikowanych prac.

Nie będę rozstrzygać, kto ma rację. To sprzeczne relacje z prywatnej rozmowy i szczegóły są naprawdę niejasne. Ale schemat nie wymaga rozstrzygnięcia, by warto go nazwać: rok nieopublikowanej pracy niezależnego badacza stał się zasobem, wokół którego dobrze finansowane laboratorium przeprowadziło wielomilionowy sprint — a teraz to niezależny badacz musi mierzyć się z pytaniami o swoją karierę.

Czy można ufać dowodowi matematycznemu napisanym przez AI?

Gdy spór o zasługi leży na stole, pozostaje trudniejsze techniczne pytanie: czy dowód się broni?

Navier–Stokes to problem z listy Millennium Prize, a standardem dowodu jest opublikowany, weryfikowalny wywód. OpenAI 8 września udostępniła 166‑stronicowy manuskrypt oraz formalizację w Lean — oba publicznie dostępne do wglądu. Niezależna recenzja jeszcze się nie odbyła.

Jeśli nie znasz Leana: to system formalnej weryfikacji dowodów, który sprawdza, czy każdy krok logiczny wynika z poprzedniego. Dowodu zweryfikowanego w Lean nie da się „zagadać” na poprawny: jeśli przechodzi, łańcuch logiczny jest spójny. Czego Lean nie robi: nie mówi, czy podejście ma sens konceptualny, czy odpowiada problemowi w rozumieniu ekspertów ani czy matematyk uznałby je za prawdziwe rozwiązanie.

Terence Tao, prawdopodobnie najwybitniejszy żyjący matematyk, ostrzegał przed tą dynamiką 5 września, jeszcze przed ogłoszeniem OpenAI. Pisząc na Mathstodon w odpowiedzi na krążące wówczas plotki, zaznaczył hipotetyczne ryzyko: „istnieje znaczny koszt alternatywny w przekształcaniu historycznie płodnego i motywującego problemu, jakim jest regularność Naviera–Stokesa, w zwykły wiralowy post w mediach społecznościowych reklamujący pewien postęp w benchmarku, zamiast faktycznie posuwać dziedzinę naprzód i rozwijać kolejne pokolenie zarówno pytań, jak i ludzi, którzy będą nad nimi pracować.” Po ogłoszeniu Tao pochwalił pracę Buckmastera–Alpöge jako „nadzwyczajne osiągnięcie” i zauważył, że ich argumenty sformalizowano w Lean. Nie poparł publicznie konkretnego dowodu zgłoszonego przez OpenAI.

Dlaczego ten spór jest większy niż jeden problem matematyczny

Plotka — nie opublikowany wynik, nie recenzja naukowa — plotka wystarczyła, by zmobilizować jedno z najlepiej dofinansowanych laboratoriów AI na świecie do wielomilionowego sprintu. OpenAI przedstawiła wynik jako dowód, jak szybko poprawiają się jej najbardziej zaawansowane systemy, czyli jako aktywo marketingowe. To problem z listy Millennium Prize użyty jako pokaz możliwości benchmarkowych przed wejściem na giełdę.

Axios postawił niewygodne pytanie wprost: co się dzieje, gdy firma dostarczająca naukowcom narzędzia AI do badań może też zmobilizować nieporównanie większe zasoby, by z nimi konkurować? Buckmaster i Alpöge przez cały rok pracy korzystali z Codexa OpenAI. Narzędzia, których badacz używa, by dojść do wyniku, mogą należeć do tej samej organizacji, która jest w stanie wyprzedzić go tymi samymi narzędziami w skali 10 000×. To nie teoria spiskowa. To cecha strukturalna obecnej chwili — scenariusz, którego się obawiano, niezależnie od tego, czy OpenAI zrobiła tu coś złego.

Jest też ironia, o której warto wspomnieć: OpenAI w sierpniu wstrzymała pewne treningi RL na granicy możliwości z uwagi na kwestie bezpieczeństwa, a we wrześniu uruchomiła nieopublikowany model z tego samego programu rozwojowego na pełnych obrotach przez 88 godzin, by gonić nagłówek o matematyce. To zestawienie nie dowodzi złej wiary, ale też nie jest bez znaczenia.

Więc czy Navier–Stokes jest rozwiązany, czy nie?

Oto, jak wygląda stan rzeczd:

Model sprintowy przyniósł wynik. Czy przyniósł Wynik — w sensie, jaki mają na myśli matematycy — to inna sprawa i na odpowiedź potrzeba znacznie więcej czasu.