OpenAI: model AI obalił hipotezę czasu wykładniczego (ETH)

Aktualizacja z 27 października 2026 roku - Anthropic publikuje własny dowód

Kilka godzin po ogłoszeniu OpenAI także Anthropic udostępnił pracę, która obala ETH. W repozytorium anthropics/formal-math na GitHubie 27 października 2026 roku pojawił się manuskrypt „A 2^o(n) Time Algorithm for 3-SAT” podpisany jako Claude (Anthropic) oraz jego formalizacja w Lean 4. Według opisu repozytorium wynik znalazł wewnętrzny, badawczy model Claude, a kod formalizacji również napisały modele AI.

Praca Anthropic opisuje deterministyczny algorytm, który rozstrzyga 3-SAT w czasie 2 do potęgi o(n), a liczbę rozwiązań wyznacza w czasie rzędu 2 do potęgi n·log log n / √log n. To ten sam rząd oszacowania, który podaje główne twierdzenie manuskryptu OpenAI. Anthropic zastrzega, że wynik jest czysto asymptotyczny i nic nie mówi o praktycznym rozwiązywaniu formuł. Według opisu Claude Opus 5.5 potrafi odtworzyć z krótkiego szkicu słabszą wersję wyniku, która również wystarcza do obalenia hipotezy.

Według TechCrunch matematyk Anthropic Levent Alpöge zasugerował, że rozwiązania OpenAI opierały się na wcześniejszych pracach. Ryan Williams z MIT, który organizuje odpowiedź środowiska informatyków, powiedział redakcji, że nie uważa algorytmu OpenAI za najlepszy możliwy. Zapytał też Dana Robertsa, szefa zespołu naukowego OpenAI, czy wynik osłabia któryś z systemów kryptograficznych. Roberts odpowiedział, że firma to sprawdziła i jest dość pewna, że nie.

W naszej ocenie dwie niezależnie ogłoszone prace z formalizacją w Lean wzmacniają tezę, że ETH jest fałszywa, ale nie zastępują recenzji. W obu przypadkach ludzie muszą jeszcze sprawdzić, czy twierdzenie zapisane w Lean odpowiada temu z manuskryptu. Repozytorium Anthropic mówi o tym wprost i odsyła do dodatku pracy, który wylicza różnice.

Co ogłosiło OpenAI

Wpis „Working with academic communities to build scientific understanding” opisuje trzy wyniki: z informatyki teoretycznej, analizy harmonicznej i kwantowej teorii pola. Wszystkie przygotował wewnętrzny, niedostępny publicznie model OpenAI. Firma nazywa takie manuskrypty surowymi danymi badawczymi, które dopiero ludzie mają przełożyć na zrozumienie.

Najwięcej uwagi przyciąga tytuł pracy z informatyki: „The Exponential Time Hypothesis is False”. Manuskrypt z 17 października, poprawiony 25 października, trafił do publicznego repozytorium openai/math na GitHubie razem z formalizacją w Lean. Lean to język, w którym komputer sprawdza każdy krok rozumowania matematycznego.

OpenAI deklaruje, że nie chce przypisywać sobie zasług naukowych za te odkrycia. Uznanie mają otrzymać badacze, którzy wyjaśnią wyniki i opiszą je dla swoich środowisk.

Czym jest hipoteza czasu wykładniczego

ETH sformułowali w 2001 roku Russell Impagliazzo i Ramamohan Paturi, a w jednej z prac także Francis Zane. Hipoteza dotyczy problemu spełnialności formuł logicznych (SAT). W wersji 3-SAT pytanie brzmi, czy da się tak ustawić wartości prawda i fałsz dla n zmiennych, aby spełnić wszystkie warunki złożone z trzech elementów. ETH zakłada, że w najgorszym przypadku wymaga to czasu rzędu 2 do potęgi n pomnożonego przez stałą.

Badacze traktowali ETH jako założenie robocze. OpenAI wylicza, że użyto go w setkach prac, by wykazać, że wiele problemów z teorii grafów, biologii obliczeniowej, baz danych czy geometrii obliczeniowej nie ma szybkich algorytmów. Takie wyniki mają postać warunkową: problem jest trudny, o ile ETH jest prawdziwa.

Co dokładnie twierdzi praca

Według streszczenia algorytm dokładnie liczy wszystkie wartościowania spełniające dowolną formułę k-CNF, czyli koniunkcję klauzul z co najwyżej k zmiennymi. Działa dla każdego stałego k równego co najmniej 2, jest deterministyczny i zużywa pamięć wielomianową. Skoro algorytm liczy rozwiązania, rozstrzyga też, czy jakiekolwiek istnieje.

Sprawdziliśmy treść manuskryptu. Główne twierdzenie podaje czas działania rzędu 2 do potęgi n·log log n / √log n, z czynnikiem wielomianowym zależnym od liczby zmiennych i klauzul. Dla formuł, w których liczba klauzul rośnie liniowo z liczbą zmiennych, wykładnik spada do n / √log n. Takie tempo wzrostu jest wolniejsze od każdej funkcji 2 do potęgi c·n, więc przeczy ETH.

Formalizacja w Lean dotyczy wersji z wykładnikiem n·(log log n)² / √log n, czyli nieco słabszego oszacowania, które również wystarcza do obalenia hipotezy. Ostrzejszą wersję autorzy dowodzą w dodatku manuskryptu.

Czego wynik nie oznacza

Nawet jeśli dowód okaże się poprawny, praca nie rozstrzyga problemu P kontra NP i nie oznacza, że wszystkie trudne problemy da się szybko rozwiązać. Opisany czas działania nadal rośnie szybciej niż dowolny wielomian. Zmienia się jedynie dolna granica, którą badacze przyjmowali za pewnik.

Wynik nie przekłada się też od razu na szybsze programy do rozwiązywania formuł logicznych, używane np. w weryfikacji układów scalonych czy planowaniu. Oszacowanie ma charakter asymptotyczny i ukrywa stałe w notacji O. OpenAI samo zaznacza, że przełożenie postępu teoretycznego na praktyczne usprawnienia będzie wymagało dużej pracy badawczej.

• Praca podważa ETH, czyli założenie, że 3-SAT nie ma algorytmu działającego w czasie 2 do potęgi o(n).
• Wynik nie rozstrzyga problemu P kontra NP.
• Dowód ma formalizację w Lean, ale nie przeszedł recenzji naukowej.
• Wpływ na praktykę jest nieznany, a autorzy nie zapowiadają szybszych solverów.
• Ponownej oceny wymagają setki prac z dolnymi ograniczeniami opartymi na ETH.

Kto sprawdzi dowód

Weryfikacją pokieruje zewnętrzna grupa: Impagliazzo i Paturi z UC San Diego oraz Ryan Williams z MIT, który według OpenAI obalał wcześniej silniejsze warianty tej hipotezy. Według The Next Web badacze podkreślili w liście do środowiska, że ich udziału nie należy traktować jako certyfikacji wyniku. Nie podpisali umów o poufności i nie otrzymują wynagrodzenia.

Grupa zażądała publikacji wszystkich surowych danych dotyczących wyniku oraz sfinansowania przez OpenAI konferencji poświęconej jego skutkom. Firma zgodziła się na oba warunki. Zespół zaprasza też innych badaczy do otwartego badania dowodu.

Dwa pozostałe wyniki z matematyki i fizyki

W analizie harmonicznej model miał udowodnić hipotezę wygładzania lokalnego (local smoothing), którą Christopher Sogge postawił w 1991 roku. Dotyczy ona zachowania fal, gdy skupiają się w jednym miejscu. Dowód we wszystkich wymiarach rozstrzygałby także hipotezę Kakeya i hipotezę restrykcji Steina. Wcześniej ludzie udowodnili wygładzanie lokalne w dwóch wymiarach (2019) i hipotezę Kakeya w trzech (2025). Tę pracę OpenAI udostępniło bez grupy opiekunów.

W fizyce OpenAI deklaruje ścisły dowód istnienia czterowymiarowych kwantowych teorii pola z polami cechowania i fermionami, w tym chromodynamiki kwantowej. Częścią pracy jest dowód istnienia czystej teorii Yanga-Millsa, związany z jednym z problemów milenijnych Instytutu Claya. Grupą opiekunów kieruje noblista David Gross, a należą do niej Michael Douglas, Arthur Jaffe, Igor Klebanov i Nikita Nekrasov. Materiałów z fizyki na razie nie opublikowano, bo grupa chce opisać wynik samodzielnie.

Ograniczenia i niewiadome

Wszystkie trzy wyniki to deklaracje firmy rozwijającej model, który je wygenerował. Żaden nie przeszedł recenzji w czasopiśmie, a model nie jest dostępny dla niezależnych badaczy. Poprzednia publikacja OpenAI z 6 października, obejmująca ponad 700 manuskryptów, już dzień później wymagała wycofania trzech prac z powodu błędu w dowodzie.

Formalizacja w Lean ogranicza ryzyko błędu w rozumowaniu, ale nie gwarantuje, że twierdzenie zapisane w Lean dokładnie odpowiada temu, co opisuje manuskrypt. Ten element sprawdzą eksperci. Nie wiadomo też, jak długo potrwa weryfikacja ani jak OpenAI uzyskało wyniki, np. ile prób i obliczeń zużył model.

Znaczenie dla polskich informatyków

ETH jest podstawowym narzędziem w złożoności parametryzowanej, dziedzinie, w której polskie ośrodki należą do czołowych na świecie. Dolne ograniczenia oparte na ETH opisuje m.in. podręcznik „Parameterized Algorithms”, którego współautorami są badacze z Uniwersytetu Warszawskiego. Jeśli dowód się obroni, część takich wyników trzeba będzie przeformułować na słabsze założenia, np. silniejszą wersję hipotezy (SETH) albo inne przypuszczenia.

W naszej ocenie badacze i doktoranci, którzy w bieżących pracach powołują się na ETH, powinni śledzić przebieg weryfikacji i na razie opisywać tę hipotezę jako podważoną, ale nie obaloną. Manuskrypt i formalizacja są dostępne publicznie, więc polskie zespoły mogą włączyć się w otwarte sprawdzanie dowodu.