W wywiadzie z 12 września 2026 roku Steven Strogatz opisał, jak AI zmienia rozumienie dowodów i zawodową tożsamość matematyków. 8 września 2026 roku OpenAI ogłosiło wynik dotyczący osobliwości w wymuszonych, trójwymiarowych, nieściśliwych równaniach Naviera–Stokesa i dołączyło do niego formalizację w Lean. To ważne zgłoszenie, ale nie jest jeszcze niezależnie zaakceptowanym rozwiązaniem problemu milenijnego. Kilka dni wcześniej Anthropic poinformowało, że Claude sformalizował istniejący dowód wielkiego twierdzenia Fermata. Oba projekty dotyczą matematyki wspieranej przez AI, lecz reprezentują zupełnie różne rodzaje osiągnięć.
Dwa różne znaczenia matematycznego przełomu
Najkrótsza odpowiedź brzmi: AI może przyspieszać badania matematyczne, ale firmowe ogłoszenie, formalizacja i zaakceptowane twierdzenie to nie to samo.
OpenAI opisało nową konstrukcję dotyczącą skończonego czasu powstania osobliwości — sytuacji, w której prędkość w analizowanym rozwiązaniu staje się nieograniczona — dla określonych równań Naviera–Stokesa. Problem istnienia i gładkości rozwiązań tych równań należy do siedmiu problemów milenijnych Clay Mathematics Institute, z nagrodą w wysokości 1 miliona dolarów za rozwiązanie każdego z nich.
Anthropic opisało natomiast pracę nad już znaną matematyką. Claude nie odkrył wielkiego twierdzenia Fermata. Sformalizował istniejący dowód związany z Andrew Wilesem i Richardem Taylorem, a w końcowej wersji wykorzystano około 29 500 twierdzeń pośrednich.
| Projekt | Cel matematyczny | Co wymaga oceny ekspertów | Rola człowieka, która pozostaje kluczowa |
| OpenAI i równania Naviera–Stokesa | Zgłoszona konstrukcja pokazująca osobliwość w skończonym czasie dla wymuszonych, trójwymiarowych, nieściśliwych równań | Czy konstrukcja dotyczy właściwego problemu i wytrzymuje niezależną analizę matematyczną | Sprawdzenie zakresu, założeń, znaczenia i poprawności rezultatu |
| Anthropic i wielkie twierdzenie Fermata | Sformalizowanie istniejącego dowodu w systemie Lean | Czy formalny zapis wiernie odwzorowuje znany dowód i przyjęte założenia systemu | Interpretacja dowodu, kontekst historyczny i ocena jego znaczenia |
Co OpenAI ogłosiło w sprawie Naviera–Stokesa
OpenAI podało, że jego systemy AI stworzyły analityczny dowód oraz formalizację Lean dla skończonej w czasie osobliwości w wymuszonych, trójwymiarowych, nieściśliwych równaniach Naviera–Stokesa. To precyzyjniejsze stwierdzenie niż hasło „AI rozwiązała Naviera–Stokesa”.
Nie oznacza ono automatycznie rozwiązania problemu milenijnego w sensie wymaganym przez matematyków. Samo zgłoszenie i dołączony kod nie zastępują niezależnej analizy, publikacji spełniającej wymagania konkursu ani szerokiej akceptacji środowiska matematycznego. Dlatego odpowiedź na pytanie, czy OpenAI rozwiązało problem Naviera–Stokesa, brzmi: nie — firma ogłosiła wynik, który wymaga dalszej oceny.
Równania Naviera–Stokesa opisują między innymi przepływ płynów. W tym przypadku nie chodzi jednak o prostą demonstrację działania modelu, lecz o bardzo szczególną konstrukcję matematyczną i o to, czy rzeczywiście odpowiada ona właściwie postawionemu problemowi.
Co Claude zrobił z dowodem Fermata
4 września 2026 roku Anthropic poinformowało, że agenci Claude sformalizowali w Lean istniejący dowód wielkiego twierdzenia Fermata. Projekt trwał 11 dni, a w jego ramach powstało około 30 300 twierdzeń pośrednich; około 29 500 wykorzystano w końcowym dowodzie.
To osiągnięcie z dziedziny formalizacji, a nie odkrycie nowego twierdzenia. Wielkie twierdzenie Fermata zostało już udowodnione przez ludzi. Wartość projektu polega na przełożeniu rozbudowanej, istniejącej argumentacji na język formalny, w którym poszczególne kroki można poddać mechanicznemu sprawdzeniu.
Różnica ma znaczenie także dla oceny pracy AI. W przypadku OpenAI pytanie dotyczy tego, czy zgłoszona konstrukcja rozwiązuje właściwy problem i jest matematycznie poprawna. W przypadku Anthropic głównym zadaniem było wierne zapisanie znanej matematyki w formalnym systemie.
Co naprawdę sprawdza Lean
Lean jest asystentem dowodzenia. Sprawdza, czy sformalizowane kroki wynikają z zakodowanych definicji, aksjomatów i założeń. To potężny filtr przeciwko błędom rachunkowym i logicznym w samym formalnym zapisie.
Nie odpowiada jednak samodzielnie na wszystkie pytania, które interesują matematyków. Mechaniczne sprawdzenie nie rozstrzyga, czy zakodowano właściwy problem, czy założenia odpowiadają intencji oryginalnego twierdzenia, czy argument jest zrozumiały dla ludzi ani czy środowisko zaakceptuje jego znaczenie.
Można to ująć prosto: Lean sprawdza, czy formalny mechanizm działa zgodnie z regułami. Matematycy muszą jeszcze ocenić, co ten mechanizm faktycznie dowodzi i dlaczego ma to znaczenie.
Przyszłość pracy matematyków
Steven Strogatz uważa, że ludzie zachowują dziś szczególną rolę jako interpretatorzy wyników generowanych przez maszyny. Nazywa tę pracę „trawieniem dowodów” — wyjaśnianiem argumentu tak, aby człowiek mógł go zrozumieć i ocenić.
To nie jest wyłącznie akademicki detal. Jeśli system potrafi wygenerować tysiące formalnych kroków, przewaga może przesunąć się z samego ich produkowania na wybór właściwego problemu, rozpoznanie dobrego kierunku i wyjaśnienie rezultatu innym badaczom.
Strogatz ostrzega zarazem, że AI może zagrozić ludzkiemu rozumieniu matematyki i zmienić źródła prestiżu w tej dziedzinie. Alex Townsend opisuje podobne napięcie z osobistej perspektywy: po 15 latach pracy badawczej uznał, że AI pomaga podejmować problemy, które wcześniej były praktycznie poza zasięgiem, ale jednocześnie zaczął czuć się zawodowo zagrożony.
To dwa obrazy tej samej zmiany. AI może zwiększać zasięg badań, a zarazem odbierać matematykowi poczucie, że to on sam znajduje się na granicy wiedzy.
Co pozostaje nierozstrzygnięte
Najważniejsza granica nie przebiega między „matematyką ludzką” a „matematyką maszynową”. Przebiega między wygenerowaniem argumentu, jego formalnym sprawdzeniem i uznaniem, że argument odpowiada właściwemu pytaniu.
W przypadku zgłoszenia OpenAI pozostają więc zasadnicze zadania: odtworzenie konstrukcji, analiza warunków, sprawdzenie zakresu twierdzenia i ocena przez niezależnych matematyków. W przypadku projektu Anthropic trzeba rozumieć, że formalizacja znanego dowodu zwiększa jego maszynową sprawdzalność, ale nie zmienia historii jego odkrycia.
Następny test: zrozumieć wynik
Wrześniowe wydarzenia pokazują, że „przełom matematyczny AI” nie jest jedną kategorią. Może oznaczać zgłoszenie nowej konstrukcji, formalizację istniejącego dowodu albo narzędzie, które pomaga człowiekowi przejść przez trudny fragment badań.
Dla czytelnika najważniejsza zasada jest prosta: nie myl formalnego sprawdzenia z akceptacją matematyczną i nie myl formalizacji z odkryciem. AI może przyspieszyć pracę, lecz sens wyniku nadal zależy od tego, czy ludzie potrafią go zrekonstruować, wyjaśnić i ocenić. To właśnie na tej granicy rozstrzygnie się, czy maszyny będą dla matematyków przede wszystkim wzmacniaczem, czy także konkurencją.
