Navier–Stokes i dowód w Leanie: wymuszone osobliwości i nieprzejrzystość laboratorium

8 września 2026 roku OpenAI oświadczyło, że jeden z jego wewnętrznych modeli, nigdy nieudostępniony publicznie, wytworzył dowód eksplozji w skończonym czasie dla trójwymiarowych nieściśliwych równań Naviera–Stokesa. Firma opublikowała dokument teoretyczny oraz publiczne repozytorium NavierStokesAndEuler, zawierające formalizację w języku Lean 4 twierdzeń dotyczących gładkich danych początkowych poddanych zewnętrznemu członowi wymuszającemu. Zgodnie z relacją laboratorium wynik obejmuje sformułowania o utracie regularności z opisu problemu przygotowanego przez matematyka Charlesa Feffermana dla Clay Mathematics Institute — nie dotyka jednak przypadku bez siły zewnętrznej, uznawanego przez środowisko naukowe za trudniejszy wariant zagadnienia. Autor oficjalnego sformułowania nazwał rozwiązanie ekscytującym, wskazując na wkład Córdoby i Martíneza-Zoroi, a firma od początku zaznaczyła, że nie zamierza ubiegać się o nagrodę miliona dolarów.

Cała operacja splata automatyzację matematyki z rytmem instytucji akademickich. Clay Mathematics Institute nadal wymienia Naviera–Stokesa wśród problemów nierozwiązanych: regulamin wymaga publikacji w kwalifikowanym miejscu, odczekania co najmniej dwóch lat od publikacji oraz ogólnej akceptacji środowiska matematycznego, a instytut jak dotąd nie wypowiedział się co do meritum. Jego prezes, Martin Bridson, przypomniał, że ocena celowo przebiega bez pośpiechu, by zagwarantować bezwzględną rzetelność. Obraz komplikuje spór o pierwszeństwo z równoległą pracą przedstawioną przez matematyka Terence'a Tao, którą jej autorzy opisują jako mocno wspieraną przez sztuczną inteligencję. Matematyk z Uniwersytetu Nowojorskiego zakwestionował przedstawioną przez laboratorium wersję kontaktów, sugerując, że do wyniku mogły przyczynić się prywatne sesje z zastrzeżonym narzędziem; firma zaprzeczyła, by miała bezpośredni wgląd w niepublikowaną pracę, przyznając zarazem, że nie może wykluczyć wpływu zdeidentyfikowanych danych użytkowych na trenowanie własnych modeli.

Repozytorium podaje instrukcje pozwalające maszynowo sprawdzić dowód, ale żadna niezależna weryfikacja nie została dotąd zakończona; poza tą kontrolą zastrzeżony charakter wykorzystanej infrastruktury uniemożliwia jakąkolwiek niezależną weryfikację kosztów i obnoszonych wskaźników wydajności. Deklarowane obliczenia — około dziesięciu tysięcy równolegle działających agentów między 1 a 5 września, 88 godzin do uzyskania dowodu i kolejne 17 na formalizację i weryfikację w Leanie — pozostają twierdzeniem firmy, którego z zewnątrz nikt nie odtworzy. Bez dostępu do kodu treningowego ani do wag systemu środowisko naukowe może potwierdzić wyłącznie formalne kroki złożone w repozytorium, a rzeczywiste warunki powtarzalności eksperymentu zostają w cieniu.

Matematyka formalna zyskała potężnego sojusznika w automatycznej kontroli kroków logicznych, ale wyścig o naukowe pierwszeństwo za pomocą zamkniętych modeli pokazuje swoje strukturalne granice. Zweryfikowanie twierdzenia jest już zadaniem dla maszyny; ustalenie przejrzystości łańcucha, który je wytworzył, wymaga wciąż rzetelności całkowicie ludzkiej.

— Olya