AI Axiom Math weryfikuje twierdzenie o 246 przerwach pierwszych w Lean

Axiom Math twierdzi, że jej system AxiomProver wyprodukował maszynowo sprawdzony dowód w Lean 4 najpotężniejszego znanego wyniku dotyczącego przerw między liczbami pierwszymi: twierdzenie, że nieskończenie wiele par liczb pierwszych różni się co najwyżej o 246. Firma opublikowała wynik 17 sierpnia 2026 jako interaktywny plan formalizacji, w którym uznano 41 wymienionych wkładów matematycznych, inżynierskich i głównych badaczy, a IEEE Spectrum jako pierwszy doniósł o tym przełomie.

Granica 246 jest obecnie granicą ludzkiej wiedzy w długotrwałym ataku na hipotezę bliźniaczych liczb pierwszych, XIX‑wieczną hipotezę, że liczby pierwsze oddzielone dokładnie dwoma występują wiecznie. Strona projektu Axiom Math opisuje pracę jako zjednoczoną formalizację artykułu Jamesa Maynarda z 2013 roku „Small gaps between primes” wraz z częścią następującej współpracy Polymath8b, która ściślejsze ograniczenie Maynarda z 600 do 246. Maszynowo sprawdzane dowody są zorganizowane w publicznej bibliotece Lean, PrimeGapsLib, a twierdzenie o 246 jest jej flagowym wynikiem.

„To twierdzenie obecnie reprezentuje granicę ludzkiej wiedzy o liczbach pierwszych” – powiedział Ken Ono, założyciel matematyczny Axiom Math.

Formalna weryfikacja oznacza przetłumaczenie dowodu na język, który mały, zaufany program zwany kernelem może sprawdzać linia po linii. Wynik nie jest absolutną gwarancją — sam opis musi być poprawnie przetłumaczony, a sprawdzacz musi być poprawny — ale usuwa z łańcucha podatność ludzkiego sędziego. Do tej pory systemy AI rywalizujące w benchmarkach matematycznych były głównie oceniane na podstawie zadań konkursowych z krótkimi, samodzielnymi dowodami; luka między tymi wynikami a formalizacją na poziomie badań była szeroka, co widać w wcześniejszych systemach, które wyróżniały się w geometrii olimpijskiej, pozostawiając badania matematyczne w dużej mierze nietknięte.

Od 70 milionów do 246

Samą hipotezę, precyzyjnie sformułowaną przez Alphonse’a de Polignaca w XIX wieku, wciąż nie udowodniono. Pierwsze skończone ograniczenie pojawiło się w 2013, kiedy Yitang Zhang udowodnił, że nieskończenie wiele par liczb pierwszych leży w odległości 70 milionów od siebie. Kilka miesięcy później Maynard wprowadził udoskonaloną metodę sita i obniżył granicę do 600 — praca, która przyczyniła się do przyznania mu Medalu Fieldsa w 2022 — a współpraca Polymath8b, w której uczestniczyli Maynard i Terence Tao, zredukowała ją do 246. Plan Axiom Math przedstawia ten postęp jako projekt, który miał zostać sformalizowany.

Formalizacja podąża za procesem opisanym przez firmę w trzech etapach. Badacze najpierw spisali dowód jako plan — każda definicja, lemat i twierdzenie otrzymały etykietę, precyzyjne sformułowanie oraz listę wyników, od których zależą — tworząc graf zależności uporządkowujący pracę. AxiomProver, wielo‑agentowy system firmy do badań matematycznych poprzez formalny dowód, wygenerował następnie maszynowo sprawdzalne dowody w Lean 4 oparte na Mathlib, społecznościowej bibliotece matematycznej, oraz na PrimeNumberTheoremAnd, istniejącym projekcie formalizacji prowadzonym przez Alexa Kontorovicha i Tao. Zespół Axiom przejrzał wygenerowany kod i zorganizował go w PrimeGapsLib.

Główne wyniki podane w bibliotece nieco wykraczają poza główne twierdzenie. Oprócz ograniczenia 246, formalizuje ona również ograniczenie Maynarda 600 oraz zawiera samodzielne wyzwanie weryfikacyjne — zbudowane wyłącznie na Mathlib, z pustym miejscem na dowód — które pozwala każdemu posiadającemu narzędzie porównawcze Lean niezależnie potwierdzić, że dowody biblioteki odpowiadają zadeklarowanym twierdzeniom. Firma ostrzega, że pełna weryfikacja może trwać godziny; skrócona wersja obejmująca pozostałe dwa wyniki działa w ciągu kilku minut.

Gdzie to plasuje się wśród roszczeń dotyczących formalizacji AI

Wynik pojawia się w roku rosnących twierdzeń o systemach AI wykonujących badania matematyczne na poziomie naukowym, z których większość opiera się na wynikach konkursowych lub krótkich dowodach. Axiom Math jest jednym z bardziej agresywnych roszczeniowiczów: AxiomProver jest uznawany za rozwiązujący wcześniej otwarte problemy, w tym prace, które firma umieściła w recenzowanych czasopismach, a systemy AI rozwiązały już kilka długoletnich problemów Erdősa. Formalizacja 246 to inny rodzaj wyniku — nie nowe twierdzenie, lecz maszynowo sprawdzona rekonstrukcja jednego z najbardziej technicznie wymagających dowodów współczesnej teorii liczb.

Najbliższym porównaniem jest wydarzenie z początku tego roku, kiedy Math, Inc. użyło swojego agenta Gaussa, aby ukończyć formalny dowód wyników pakowania sfer Maryny Viazovskiej, laureatki Medalu Fieldsa, w wymiarach 8 i 24. Sidharth Hariharan, doktorant Carnegie Mellon, który prowadził ludzką pracę nad planem tej formalizacji i jest teraz stażystą w Axiom Math oraz wymienionym współtwórcą matematycznym projektu 246, twierdzi, że nowy wynik jest bardziej wszechstronnym osiągnięciem. Jego argumentacja, jak opisuje, polega na tym, że Axiom zbudował bibliotekę z myślą o ponownym użyciu: zamiast jednorazowej formalizacji jednego dowodu, PrimeGapsLib jest utrzymywaną biblioteką wyników dotyczących przerw pierwszych, przeznaczoną do wspierania przyszłych prac formalizacyjnych i badań.

To rozróżnienie ma znaczenie dla sposobu odbioru wyniku. Jednorazowa weryfikacja pokazuje, że system może poradzić sobie z jednym trudnym dowodem. Biblioteka natomiast demonstruje coś bliższego infrastrukturze — wielokrotnego użytku formalne narzędzia, na których mogą opierać się inne wyniki — co jest kierunkiem, w którym zmierzają systemy formalnego dowodzenia, przechodząc od rozwiązywania ćwiczeń do sprawdzania prawdziwej matematyki. Twierdzenie o zdolnościach opiera się tutaj na artefaktach, które są publiczne i możliwe do ponownego uruchomienia, a nie na wyniku benchmarku: plan, kod Lean oraz wyzwanie porównawcze zaprojektowane tak, aby zewnętrzni badacze mogli samodzielnie zweryfikować dowody.

Ono przedstawia matematykę jako poligon testowy dla większej ambicji. Jeśli własności oprogramowania — czy program się kończy, czy jego wynik jest poprawny dla każdego wejścia — mogą być wyrażone jako precyzyjne stwierdzenia matematyczne, wtedy systemy wywodzące się z AxiomProver mogłyby je formalnie udowadniać, argumentuje, wskazując w kierunku weryfikacji kodu generowanego przez AI, który zaczyna obsługiwać infrastrukturę, finanse i systemy bezpieczeństwa.

„Świat wkrótce będzie działał na kodzie komputerowym, którego nikt nie przeczytał” – powiedział Ono. „AI jest już tutaj i nie możemy już odwrócić wzroku — formalizacja dowodów jest poligonem testowym dla rozwiązania tego, co uważam za najważniejsze wyzwanie, przed którym stanie nasz gatunek wobec AI”.

Na razie dostarczany rezultat jest węższy i możliwy do sprawdzenia: plan autorstwa 41 autorów, publiczna biblioteka Lean oraz maszynowo zweryfikowany dowód, że liczby pierwsze oddalone od siebie o co najwyżej 246 nigdy się nie wyczerpują — najbliższy zweryfikowany sąsiad hipotezy bliźniaczych liczb pierwszych oraz najgłębszy element badań matematycznych, jaki dotąd sprawdził system AI od początku do końca.