Zespół Axiom Math po raz pierwszy przepuścił przez maszynę pełny dowód twierdzenia 246, czyli wyniku wyznaczającego dzisiejszą granicę wiedzy o liczbach pierwszych. Firma Cariny Hong nie robi tego dla samej matematyki, tylko po to, żeby nauczyć się formalnie potwierdzać poprawność kodu generowanego przez sztuczną inteligencję.
Kluczowe fakty:
- System AxiomProver firmy Axiom Math przeprowadził formalną weryfikację maszynową pełnego dowodu twierdzenia 246, które stwierdza, że istnieje nieskończenie wiele par liczb pierwszych różniących się o 246 – jest to obecnie najbliższy punkt do nierozwiązanej od XIX wieku hipotezy o liczbach bliźniaczych.
- AxiomProver to autonomiczny system wieloagentowy zamieniający zdania matematyczne w dowody sprawdzalne maszynowo, a jego pierwotnym celem jest nauka formalnego potwierdzania poprawności kodu generowanego przez sztuczną inteligencję.
- W odróżnieniu od wcześniejszych jednorazowych formalizacji, Axiom Math celowo budował przy twierdzeniu 246 elementy wielokrotnego użytku, tworząc bibliotekę wyników nadającą się do ponownego wykorzystania w kolejnych projektach.
Informację opisał wczoraj IEEE Spectrum. Za weryfikacją stoi AxiomProver, autonomiczny system wieloagentowy, który zamienia zdania matematyczne w dowody sprawdzalne maszynowo. Twierdzenie 246 mówi, że istnieje nieskończenie wiele par liczb pierwszych różniących się o 246. Brzmi jak ciekawostka. Jest to jednak najbliższy punkt, do jakiego matematycy zdołali podejść pod hipotezę o liczbach bliźniaczych, otwartą od XIX wieku.
Chcesz czytać więcej treści związanych z AI?
Dodaj AIPORT.pl do preferowanych źródeł Google
Co dokładnie zrobił AxiomProver
Weryfikacja formalna polega na tym, że komputer sprawdza maszynowo czytelną wersję dowodu, krok po kroku, bez litości dla luk w rozumowaniu. To nie jest gwarancja stuprocentowa i za chwilę wyjaśnię dlaczego. Ale w praktyce nic bliższego pieczątce dziś nie mamy.
Ken Ono, założycielski matematyk Axiom Math, tłumaczy wagę wyniku krótko: „To twierdzenie wyznacza dziś granicę ludzkiej wiedzy o liczbach pierwszych” / „This theorem currently represents the threshold of human knowledge about prime numbers.”
To nie pierwszy taki wynik firmy. AxiomProver rozwiązywał już wcześniej otwarte problemy i formalizował dowody, ale ten przypadek jest zbudowany inaczej. Sidharth Hariharan, doktorant Carnegie Mellon University, obecnie stażysta w Axiom Math, kierował wcześniej pracami ludzi nad planem formalizacji nagrodzonego Medalem Fieldsa dowodu Maryny Wiazowskiej dotyczącego upakowania sfer w 8 i 24 wymiarach. Tamtą formalizację przeprowadził agent Gauss konkurencyjnej firmy Math, Inc. Hariharan uważa, że praca nad twierdzeniem 246 jest bardziej kompleksowa i użyteczna, bo nie było to podejście jednorazowe. Axiom Math celowo budował elementy, które da się użyć ponownie. Efektem jest biblioteka wyników o odstępach między liczbami pierwszymi, opublikowana jako PrimeGapsLib, a twierdzenie 246 stanowi jej sztandarowy rezultat.
Skąd się wzięła liczba 246
Liczby pierwsze bliźniacze to pary różniące się o dwa: 3 i 5, 5 i 7, 11 i 13, 17 i 19. Im dalej od zera, tym rzadziej się pojawiają. Alphonse de Polignac sformułował w XIX wieku przypuszczenie, że mimo to nigdy się nie kończą. Dowodu nadal nie ma.
Droga do liczby 246 wyglądała tak:
- 2013, Yitang Zhang udowodnił, że istnieje nieskończenie wiele par liczb pierwszych oddalonych od siebie o 70 milionów. Pierwszy wyłom po ponad stu latach.
- Kilka miesięcy później, James Maynard z University of Oxford, inną techniką, zbił ten odstęp z 70 milionów do 600. Ten wynik znacząco przyczynił się do przyznania mu Medalu Fieldsa w 2022 roku.
- Współpraca Polymath8b, w której Maynard pracował razem z Terence’em Tao z UCLA, zeszła do 246.
- Sierpień 2026 przynosi pierwszą maszynową weryfikację tego dowodu.
Od 246 do docelowej dwójki wciąż daleko. Ale to właśnie ten wynik AxiomProver potwierdził jako poprawny.
Weryfikator to też program, a programy mają błędy
Tu dochodzimy do niewygodnej części. Trzy tygodnie temu środowisko formalizacji przeżyło zimny prysznic. 25 lipca Ramana Kumar opublikował na GitHubie repozytorium z „obaleniem” hipotezy Collatza, przygotowanym z pomocą AI. Dowód przeszedł przez rdzeń Leana. Przeszedł też przez nanoda, niezależny weryfikator napisany w Ruście przez Chrisa Baileya. I był fałszywy.
Kiran Gopinathan sprowadził 28 lipca całość do minimalnego dowodu fałszu i zgłosił błąd numer 14576. Poprawka poszła godzinę po zgłoszeniu. Leonardo de Moura, twórca Leana, opisał wszystko w publicznym rozliczeniu: rdzeń gubił kontrolę typów przy zagnieżdżonych typach indukcyjnych z parametrami fantomowymi, a nanoda miała drugi, zupełnie niezwiązany błąd. Dwie niezależne implementacje, dwie różne dziury, ten sam skutek.
W rozmowie z Machine Learning Street Talk de Moura powiedział wprost: „To będzie się powtarzać. Modele AI są naprawdę dobre w wykorzystywaniu błędów poprawności w rdzeniach weryfikatorów” / „This is going to keep happening. AIs are really good at exploiting soundness bugs in the kernels.”
Zapis tej rozmowy: twitter.com/MLStreetTalk
Patrzę na to z dwóch stron. Z jednej mamy realny postęp: biblioteka wyników o odstępach między liczbami pierwszymi, z której da się korzystać dalej, to coś więcej niż jednorazowy pokaz siły. Z drugiej lipcowa wpadka Leana przypomina, że weryfikator też jest programem napisanym przez ludzi i też ma błędy.
Pytanie, które mnie nurtuje, brzmi inaczej niż w większości komentarzy, jakie czytałem po tej sprawie. Nie chodzi o to, czy maszyna udowodni twierdzenie szybciej od człowieka. Chodzi o to, kto weźmie odpowiedzialność, gdy kod przepuszczony przez taki system trafi do banku albo do szpitala i zawiedzie. Zaufanie do dowodu formalnego przenosi się wtedy z matematyki na rdzeń weryfikatora, na jego implementację i na ludzi, którzy ją utrzymują.
To wciąż jest zaufanie. Tylko przesunięte o jeden poziom niżej i schowane głębiej, tam, gdzie mało kto zagląda.
Piotr Wolniewicz, Redaktor Naczelny AIPORT.pl
Opisz krótko, czego potrzebujesz. Jesteśmy największym HUB-em AI w Polsce — w naszej bazie znajdziesz blisko 500 zweryfikowanych firm specjalizujących się w AI. W Twoim imieniu poprosimy 3-5 dopasowanych wykonawców o kontakt w ciągu 48 godzin.
Kod, którego nikt nie przeczytał
Teoria liczb, w której osadzone jest twierdzenie 246, leży pod całą współczesną kryptografią i cyberbezpieczeństwem. Techniki sformalizowane przy okazji tej pracy mogą się więc przydać do sprawdzania konkretnych mechanizmów ochrony danych.
Ono myśli jednak szerzej. Formalizację dowodów traktuje jako etap przejściowy w drodze do weryfikowania kodu pisanego przez modele. Jeśli własności programu, na przykład to, czy algorytm w ogóle się zatrzyma albo czy wynik jest poprawny dla dowolnych danych wejściowych, da się zapisać jako precyzyjne zdania matematyczne, technologie wyrosłe z AxiomProvera nadają się do ich udowodnienia.
„Świat zaraz zacznie działać na kodzie, którego nikt nie przeczytał” / „The world is about to run on computer code that nobody has read.” Ono nazywa formalizację dowodów poligonem doświadczalnym dla największego, jego zdaniem, wyzwania związanego ze sztuczną inteligencją.
Za tą deklaracją stoją pieniądze. Axiom Math powstało w marcu 2025 roku, założyła je Carina Hong, absolwentka MIT, która porzuciła studia doktoranckie na Stanfordzie. Po rundzie zalążkowej wartej 64 miliony dolarów firma zebrała w marcu 2026 roku 200 milionów w rundzie A prowadzonej przez Menlo Ventures, przy wycenie 1,6 miliarda dolarów po transakcji. Łącznie ponad ćwierć miliarda dolarów. Ono zrezygnował w grudniu 2025 roku z profesury na University of Virginia, żeby dołączyć do zespołu. W tym samym miesiącu AxiomProver zdobył komplet punktów na konkursie Putnama.
Skala ekosystemu wokół Leana też robi wrażenie. Mathlib, biblioteka utrzymywana przez społeczność, zawiera ponad 210 tysięcy formalnie zweryfikowanych twierdzeń zebranych przez blisko dekadę pracy setek matematyków z całego świata.
Za każdą polską firmą AI stoi konkretny człowiek z imieniem i nazwiskiem, często ten sam w kilku miejscach naraz, i to właśnie ludzie, nie tabelki finansowania, są prawdziwym bohaterem tego artykułu.
Mizar z Białegostoku, czyli polski ślad sprzed pół wieku
Ta historia ma polski wątek, o którym rzadko się pamięta, a szkoda. Andrzej Trybulec zaprezentował system Mizar 14 listopada 1973 roku, dekady przed Leanem, Coqiem i Isabelle. Projekt rozwijany jest do dziś na Uniwersytecie w Białymstoku, we współpracy z Uniwersytetem Shinshū w Japonii.
Mizar Mathematical Library, czyli zbiór zweryfikowanych maszynowo definicji, twierdzeń i dowodów, budowany jest od 1989 roku. W 2012 roku liczył ponad 1100 artykułów formalnych, ponad 50 tysięcy twierdzeń i 10 tysięcy definicji. Nowe prace, po recenzji i automatycznym sprawdzeniu, trafiają do Journal of Formalized Mathematics. Trybulec zmarł w 2013 roku w Białymstoku.
Piszę o tym nie z kronikarskiego obowiązku. Amerykańskie firmy wyceniane na miliardy dolarów rozwiązują dziś problem, który w Polsce postawiono ponad pięćdziesiąt lat temu i nad którym cały czas pracuje krajowy ośrodek akademicki. Jeśli formalna weryfikacja kodu naprawdę stanie się warstwą infrastruktury, kompetencje zgromadzone w Białymstoku będą jednym z niewielu polskich zasobów w tej dziedzinie, których nie da się szybko odtworzyć w innym kraju. Pytanie brzmi, czy ktokolwiek w Warszawie to zauważy, zanim rynek rozdzieli role.
Dla polskich firm produkujących oprogramowanie sprawa ma jeszcze jeden wymiar. Coraz większa część kodu powstaje z pomocą modeli językowych, a klienci z sektorów regulowanych, bankowości, medycyny, energetyki, zaczną prędzej czy później pytać o dowody poprawności, nie o zapewnienia. Wtedy przyda się ktoś, kto rozumie, jak taki dowód wygląda od środka.
To zresztą kolejny w tym roku przypadek, gdy sztuczna inteligencja przesuwa granice w matematyce. W lipcu opisywaliśmy obalenie hipotezy Jacobiego przy pomocy modelu Claude Fable 5. Różnica polega na tym, że tam model znalazł kontrprzykład, a tutaj maszyna sprawdziła cudzy dowód. Drugie zadanie jest nudniejsze i znacznie ważniejsze dla tego, co się wydarzy w oprogramowaniu w najbliższych latach.
Źródła i metodologia
Artykuł powstał na podstawie analizy redakcji AIPORT.pl oraz materiału IEEE Spectrum autorstwa Benjamina Skuse’a z dnia 17.08.2026, publicznego rozliczenia błędu rdzenia Leana opublikowanego przez Leonarda de Mourę oraz repozytorium PrimeGapsLib na GitHubie. Dane o finansowaniu Axiom Math pochodzą z relacji Fortune i Madrona Venture Group, dane o systemie Mizar z materiałów Uniwersytetu w Białymstoku i publikacji naukowych o Mizar Mathematical Library. Cytaty Kena Ono, założycielskiego matematyka Axiom Math, oraz Leonarda de Moury, twórcy systemu Lean, zostały zweryfikowane z oryginalnym anglojęzycznym materiałem źródłowym. Komentarz redakcyjny i ocena kontekstu branżowego: Piotr Wolniewicz, Redaktor Naczelny AIPORT.pl. Artykuł będzie aktualizowany w miarę pojawiania się nowych informacji o formalnej weryfikacji dowodów i kodu generowanego przez AI.
