OpenAI twierdzi, że rozwiązało problem milenijny. Matematycy pytają, skąd wziął się pomysł

👁 128 przeczytań

8 września 2026 OpenAI ogłosiło, że jego wewnętrzny system rozwiązał problem Naviera-Stokesa, jeden z sześciu nierozwiązanych Problemów Milenijnych, za które Instytut Claya wyznaczył nagrodę miliona dolarów. Dowód opublikowano razem z formalizacją w języku Lean. W ciągu kilkunastu godzin sukces został przykryty przez spór o to, skąd wziął się pomysł na rozwiązanie.

Co konkretnie ogłoszono

System wieloagentowy, sterowany nieudostępnionym publicznie modelem opisywanym jako znacznie mocniejszy od GPT-6 Astra, wskazał osobliwość w trójwymiarowych równaniach Naviera-Stokesa. Innymi słowy: pokazał, że rozwiązanie może w skończonym czasie przestać być gładkie, czyli że równania opisujące ruch płynów potrafią się w pewnym momencie „rozerwać”.

Dwie rzeczy warto zapamiętać, bo giną w nagłówkach. Po pierwsze, OpenAI zapowiedziało, że nie będzie ubiegać się o nagrodę. Po drugie, strona Instytutu Claya nadal wykazuje ten problem jako nierozwiązany, bo procedura przyznania nagrody wymaga publikacji i dwóch lat weryfikacji przez środowisko.

Zarzut pierwszy: skąd wziął się pomysł

Rok wcześniej matematyk Tristan Buckmaster z Courant Institute na NYU pracował razem z Leventem Alpöge nad tym samym problemem, rozwijając podejście Diega Córdoby i Luisa Martíneza-Zoroi. 15 sierpnia udowodnili, że prostsze równania Eulera rzeczywiście wybuchają, co jest krokiem w stronę Naviera-Stokesa. Korzystali przy tym z modeli obu firm: Anthropic i OpenAI.

Buckmaster wydał oświadczenie przed komunikatem OpenAI. Napisał w nim, że wraz z Alpöge doszli do niemal identycznego rozwiązania jednej z części problemu. I postawił pytanie, które zapaliło całą sprawę: czy wewnętrzny model OpenAI miał dostęp do jego rozmów w Codeksie, gdzie trzymał notatki z tej pracy.

„Zapytałem, czy model był trenowany na naszych sesjach w Codeksie albo miał do nich dostęp. Powiedziano mi, że model nie sięgał po dane użytkowników. Zapytałem ponownie, o trenowanie, i nie dostałem odpowiedzi.”

Tristan Buckmaster, z oświadczenia opublikowanego na stronie Courant Institute

Zwróć uwagę na konstrukcję tej odpowiedzi. Firma zaprzeczyła jednej rzeczy, o którą pytano, i przemilczała drugą. To nie jest to samo co zaprzeczenie obu.

Odpowiedź firmy jest tu najciekawsza. OpenAI zapewniło, że model nie przeglądał danych użytkowników, ale odmówiło odpowiedzi na pytanie, czy notatki trafiły do zbioru treningowego. To są dwie różne rzeczy i zaprzeczenie pierwszej nie wyklucza drugiej.

Zarzut drugi: moment startu

Według OpenAI prace ruszyły 1 września, po tym jak badacze firmy usłyszeli plotki, że dwa Problemy Milenijne zostały rozwiązane. Firma podaje to jako dowód szybkości. Można to jednak przeczytać inaczej: wielkie laboratorium rzuca ogromne zasoby na problem dokładnie wtedy, gdy dowiaduje się, że ktoś inny jest blisko.

Terence Tao, jeden z najbardziej cenionych żyjących matematyków, zwrócił uwagę właśnie na ten mechanizm. Ostrzegł, że akcje uruchamiane na sygnał o cudzych postępach mogą zniechęcić badaczy do dzielenia się kierunkami pracy, a to jest waluta, na której stoi matematyka.

Zarzut trzeci: nacisk w sprawie autorstwa

Pojawiły się doniesienia, że OpenAI próbowało wpłynąć na to, komu przypisane zostanie osiągnięcie w publikacji. Część matematyków użyła w tym kontekście słów o oszustwie i zastraszaniu. Firma zaprzeczyła zarzutom na konferencji prasowej.

Do tego dochodzi różnica w postępowaniu, którą trudno zbyć. Buckmaster opublikował swoją pracę razem z kodem w Lean. OpenAI w momencie ogłoszenia nie udostępniło szczegółów dowodu, plik i odnośnik do formalizacji dołożono później.

Czego weryfikacja w Lean nie rozstrzyga

To jest punkt najczęściej mylony, więc warto go rozpisać. Lean to język, w którym dowód zapisuje się tak, że komputer sprawdza każdy krok. Jeśli formalizacja przechodzi, rozumowanie jest poprawne w sensie logicznym. I tyle.

Czego Lean nie sprawdzi: czy sformalizowane twierdzenie odpowiada temu, o co pyta problem milenijny w sformułowaniu Charlesa Feffermana. Można poprawnie udowodnić twierdzenie sąsiednie, nieco słabsze albo obwarowane założeniem, którego oryginał nie dopuszcza. Rozstrzygnięcie tego wymaga ludzi, którzy przeczytają, co dokładnie zostało zapisane.

Pierwsze takie odczytanie już nastąpiło. Stan Palasek z Princeton wskazał przeszkodę w konstrukcji opartej na niestabilnościach o bardzo odległych częstotliwościach. Tao przyjął tę uwagę i zaproponował prostszy model do prześledzenia tych oddziaływań.

Warto przy tym oddać głos człowiekowi, który ten problem sformułował. Charles Fefferman z Princeton, autor oficjalnego sformułowania zadania dla Instytutu Claya, zareagował krótko: „Byłem zachwycony, że problem został rozwiązany”. Sceptycyzm środowiska nie dotyczy więc samej możliwości, że wynik jest prawdziwy, tylko trybu, w jakim powstał i został ogłoszony.

Zarzut czwarty, najpoważniejszy: czarna skrzynka

Tao sformułował go jeszcze przed ogłoszeniem, 5 września, gdy pisał, że nie zna żadnych znaczących postępów w tej sprawie. Jego teza brzmi mniej więcej tak: nawet gdyby autonomiczny system w pełni rozwiązał problem, ale proces poszukiwania pozostał nieprzejrzysty, wartość takiego wyniku dla matematyki jest bliska zeru.

Powód jest prosty i nie ma nic wspólnego z niechęcią do maszyn. Matematyka nie zbiera odpowiedzi, tylko metody. Dowód, którego nie da się prześledzić, nie uczy niczego, co dałoby się użyć przy następnym problemie. Tao krytykował też osobno ukrywanie nieudanych prób i samego przebiegu poszukiwań, czyli tego, co w normalnej pracy naukowej bywa cenniejsze od wyniku.

Cytat, który mówi więcej niż cały spór

W relacji Quanta Magazine Buckmaster opisuje pierwszy dowód, jaki dostał od modelu językowego, i robi to bez cienia uprzejmości:

„Pierwszy dowód wygenerowany przez model, który przysłał mi Levent, był najstraszniejszy, jaki kiedykolwiek czytałem. Można to określić tylko jako AI slop. Przepraszam za to.”

Tristan Buckmaster, Quanta Magazine

To ten sam człowiek, który kilka miesięcy później doszedł do rozwiązania z pomocą tych narzędzi. do wyniku niemal identycznego z ogłoszonym przez OpenAI. Odległość między „bełkot” a „prawie to samo, co ogłosiła firma warta setki miliardów” zmieściła się w jednym roku.

Po drugiej stronie stoi Diego Córdoba, którego podejście rozwijali obaj badacze. Zapytany o korzystanie ze sztucznej inteligencji odpowiedział zdaniem, które obiegło środowisko:

„Nie używam AI. Mam Luisa.”

Diego Córdoba o współpracy z Luisem Martínezem-Zoroą, Quanta Magazine

Co z tego wynika

Trzy rzeczy są pewne: ogłoszenie padło, formalizacja istnieje, a nagrody firma nie chce. Reszta wymaga miesięcy. Zanim ktokolwiek ogłosi rozstrzygnięcie, musi zajść to samo, co przy każdym dużym dowodzie: niezależni matematycy przeczytają zapis i orzekną, czy dowodzi tego, o co pytano.

Osobno zostaje pytanie, które dotyczy każdego, kto pracuje z tymi narzędziami: czy da się bezpiecznie używać modeli czołowych laboratoriów do pracy nad niepublikowanymi wynikami. Sprawa Buckmastera nie odpowiada na nie twierdząco ani przecząco, ale samo jej postawienie już zmienia zachowania. Ile ta operacja kosztowała i jak była zbudowana, rozbieram w osobnym tekście o rachunku za dziesięć tysięcy agentów.

Najczęściej zadawane pytania

Czy OpenAI dostanie nagrodę miliona dolarów za rozwiązanie problemu Naviera-Stokesa?

Nie, ponieważ OpenAI zapowiedziało, że nie będzie ubiegać się o nagrodę. Dodatkowo strona Instytutu Claya nadal wykazuje ten problem jako nierozwiązany, gdyż procedura przyznania nagrody wymaga publikacji i dwóch lat weryfikacji przez środowisko.

Dlaczego matematycy kwestionują ogłoszenie OpenAI mimo formalizacji dowodu w języku Lean?

Lean sprawdza jedynie poprawność logiczną każdego kroku dowodu, ale nie weryfikuje, czy sformalizowane twierdzenie odpowiada dokładnie temu, o co pyta problem milenijny w sformułowaniu Charlesa Feffermana. Można poprawnie udowodnić twierdzenie nieco słabsze lub obwarowane założeniem, którego oryginał nie dopuszcza - rozstrzygnięcie tego wymaga ludzi, którzy przeczytają, co dokładnie zostało zapisane.

Jakie pytanie o dostęp do danych postawił Tristan Buckmaster wobec OpenAI?

Buckmaster zapytał, czy wewnętrzny model OpenAI był trenowany na jego sesjach w Codeksie, gdzie trzymał notatki ze swojej pracy nad tym problemem, albo miał do nich dostęp. Firma zapewniła, że model nie przeglądał danych użytkowników, ale odmówiła odpowiedzi na pytanie, czy notatki trafiły do zbioru treningowego.