Jak sztuczna inteligencja OpenAI źle przetłumaczyła własny matematyczny dowód Naviera-Stokesa na kod

Co ogłosiła OpenAI

8 września 2026 roku OpenAI ogłosiła, że jej wewnętrzny system wieloagentowy stworzył dowód dotyczący problemu istnienia i gładkości rozwiązań równań Naviera-Stokesa, jednego z siedmiu Problemów Nagród Milenijnych ze statuetką w wysokości 1 miliona dolarów z Matematycznego Instytutu Claya, według witryny śledzenia sztucznej inteligencji implicator.ai. Firma poinformowała, że około 10 000 agentów pracowało przez 88 godzin od 28 sierpnia, generując 2,7 miliona wiadomości od agentów i około 130 miliardów tokenów wyjściowych, zanim oddzielny model, opisywany jako GPT-6 Astra, spędził dodatkowe 17 godzin na formalnym sprawdzeniu argumentu w języku dowodów Lean.

Rezultatem był rękopis w języku naturalnym zatytułowany «Skończone czasy wybuchu dla Naviera-Stokesa», towarzyszony projektowi Lean mającemu na celu umożliwienie komputerom sprawdzenia każdego kroku logicznego, według implicator.ai i artykułu na arXiv, który później przeanalizował tę pracę.

Odkrycia dotyczące błędów tłumaczenia

Artykuł opublikowany na serwerze preprintów arXiv pod tytułem «Navier-Stokes Lost in Translation» napisany przez matematyków Aleksandra Bastounisa, Fabiana Circellego i Andersa C. Hansena zbadał, czy kod Lean OpenAI faktycznie odpowiada argumentowi matematycznemu w artykule w języku naturalnym. Autorzy rozróżniają między dowodem Lean, który jedynie się kompiluje, a dowodem, który jest semantycznie wierny pierwotnej argumentacji, twierdząc, że drugi rodzaj jest znacznie trudniejszy do gwarancji niż pierwszy.

Artykuł wymienia konkretne niezgodności. W jednym przypadku Lemat 8.6 artykułu w języku naturalnym wymaga ograniczenia pochodnych przy użyciu czterech dodatkowych rzędów wejścia, napisanych m+4, ale odpowiednie twierdzenie Lean zamiast tego wymaga pięciu dodatkowych rzędów, m+5 — silniejszego warunku niż ten podany w artykule. W innym przypadku równanie 10.19 rękopisu ogranicza wyraz strumienia ciśnienia, używając tylko jednej zmiennej, zwanej B_R, podczas gdy wersja Lean tego samego ograniczenia również zależy od drugiej zmiennej, A_R, pochodzącej z innej techniki matematycznej.

Autorzy dochodzą do wniosku, że pomyślna kompilacja pliku Lean tylko pokazuje, że istnieje jakiś słuszny dowód dla sformułowanego twierdzenia, a nie że jest to ten sam dowód opisany słowami. Piszą, że kod Lean OpenAI często nakłada silniejsze warunki na granice różnych funkcji niż odpowiadające im wyniki w artykule w języku naturalnym, i zalecają, aby formalizacje Naviera-Stokesa OpenAI i powiązane formalizacje równań Eulera przeszły tę samą recenzję naukową, którą otrzymują tradycyjne dowody, zanim będą godne zaufania.

Odrębny spór: który problem został rozwiązany?

Niezależnie od kwestii tłumaczenia, wielu matematyków kwestionowało, czy OpenAI rozwiązała wersję Naviera-Stokesa, którą najbardziej interesuje większość badaczy. Oficjalne sformułowanie problemu Matematycznego Instytutu Claya z 2000 roku, napisane przez Charlesa Feffermana, zawiera opcję oznaczoną literą C, która pozwala na gładki zewnętrzny wyraz wymuszenia, podczas gdy większość matematyków skupiała się na przypadku bez wymuszenia, jak donosi Scientific American.

Dowód OpenAI dotyczy opcji C. Luis Silvestre z Uniwersytetu w Chicago i jego współpracownicy opublikowali artykuł argumentujący, że mechanizm wybuchu OpenAI nie może działać po usunięciu siły zewnętrznej, jak donosi Scientific American.

Część szerszego wzorca kontroli

Sprawdzanie matematycznych twierdzeń OpenAI nie jest nic nowego. W październiku 2025 roku ówczesny wiceprezydent OpenAI Kevin Weil powiedział, że GPT-5 rozwiązała dziesięć wcześniej nierozwiązanych problemów Erdősa i poczynił postępy w jedenastu następnych; matematycy, w tym Thomas Bloom, powiedzieli, że wyniki już istniały w opublikowanej literaturze, a Weil wycofał post, jak donosi TechCrunch. Kiedy OpenAI ogłosiła w maju 2026 roku, że model rozumowania obalił hipotezę geometrii Erdősa z 1946 roku, opublikowała wspierające oświadczenia matematyków Nogi Alona, Melanie Wood i Thomasa Bloom'a — tego samego Bloom'a, który wcześniej zidentyfikował błąd — wraz z twierdzeniem, jak donosi TechCrunch.

7 października 2026 roku OpenAI opublikowała 372 wyniki matematyczne wygenerowane przez sztuczną inteligencję na GitHubie, każdy mający na celu rozwiązanie otwartego problemu lub dokonanie istotnego postępu w jego kierunku, większość wyprodukowana z jednego monitu do wewnętrznego modelu przy koszcie około trzech godzin czasu obliczeniowego ChatGPT Pro każdy, jak donosi the-decoder. Dwudziestu pięciu laureatów Medalu Fieldsa podpisało otwarty list ostrzegający, że masowa produkcja rzeczywistych zdań matematycznych ryzykowała raczej zniszczeniem tego pola niż jego postępem, zgodnie z tym samym raportem, który zauważył, że większość wyników nie przeszła standardowej recenzji naukowej.

Gdzie aktualnie stoi to twierdzenie

Matematyczny Instytut Claya nadal wymienia Naviera-Stokesa wśród swoich nierozwiązanych Problemów Nagród Milenijnych, jak donosi implicator.ai. Prezes Instytutu Martin Bridson powiedział, że ogłoszenie było ekscytujące, ale że każda formalna ocena byłaby bezpośrednia i rygorystyczna.