Firma Axiom Math ogłosiła, że jej system AI AxiomProver zweryfikował formalnie „twierdzenie 246” — jeden z najtrudniejszych dotąd sformalizowanych wyników teorii liczb. To najbliższy dotychczas dowód w kierunku hipotezy liczb bliźniaczych, a maszyna sprawdziła jego poprawność krok po kroku.
Najważniejsze w skrócie
- Axiom Math sformalizował „twierdzenie 246” swoim systemem AxiomProver.
- Twierdzenie: istnieje nieskończenie wiele par liczb pierwszych w odstępie 246.
- Pierwotny dowód: James Maynard i Terence Tao (projekt Polymath8b).
- AxiomProver to autonomiczny, wieloagentowy system zamieniający twierdzenia na dowody sprawdzalne maszynowo.
- Powstała reużywalna biblioteka PrimeGapsLib udostępniona na GitHub.
Najbliżej liczb bliźniaczych
Hipoteza liczb bliźniaczych mówi, że istnieje nieskończenie wiele par pierwszych różniących się o 2 (jak 11 i 13). Nikt jej nie udowodnił. „Twierdzenie 246” to najbliższy przyczółek: dowodzi nieskończenie wielu par w odstępie co najwyżej 246.
Wynik narodził się w projekcie Polymath8b, który zbił granicę z 70 milionów (2013) przez 600 aż do 246 — w oparciu o prace laureatów Medalu Fieldsa Jamesa Maynarda i Terence'a Tao. To realny, głęboki fragment współczesnej matematyki, a nie zabawkowy przykład.
Znaczenie symboli
- …
- odstęp między kolejnymi liczbami pierwszymi
- …
- wartość, do której odstępy schodzą nieskończenie często
| Etap | Maksymalny odstęp |
|---|---|
| 2013 — pierwszy wynik | 70 000 000 |
| 2013 — dalsza poprawa | 600 |
| twierdzenie 246 | 246 |
To twierdzenie wyznacza dziś granicę ludzkiej wiedzy o liczbach pierwszych.
Ken Ono, matematyk-założyciel w Axiom Math.
Jak działa AxiomProver
AxiomProver to autonomiczny system wieloagentowy, który zamienia zapis matematyczny na dowód sprawdzalny maszynowo — proces zwany autoformalizacją. Zamiast liczyć na to, że recenzent-człowiek nie przeoczy błędu, formalna weryfikacja daje maszynowo potwierdzoną pewność każdego kroku.
Przy tej skali to najpoważniejsze osiągnięcie AxiomProvera do tej pory. Pracę prowadził m.in. Sidharth Hariharan, doktorant Carnegie Mellon University i stażysta w Axiom Math. Efektem jest nie tylko sam dowód, ale i biblioteka PrimeGapsLib na GitHub, z której mogą korzystać inni.
Dlaczego to ważne?
Formalna weryfikacja trudnego twierdzenia pokazuje, że AI dojrzewa z generatora prawdopodobnych odpowiedzi do narzędzia dającego twardą, sprawdzalną pewność.
To istotne poza matematyką: te same techniki mogą w przyszłości dowodzić poprawności i bezpieczeństwa kodu — w tym kodu pisanego przez AI. W świecie, w którym coraz więcej oprogramowania powstaje maszynowo i nikt go nie czyta w całości, formalny dowód staje się jednym z niewielu wiarygodnych sposobów kontroli.
Co dalej?
- Biblioteka PrimeGapsLib jest dostępna na GitHub i może posłużyć do kolejnych formalizacji w teorii liczb.
- Axiom Math wskazuje weryfikację kodu generowanego przez AI jako docelowe zastosowanie tych technik.
- Kolejnym testem będzie formalizacja wyników jeszcze bliższych hipotezie liczb bliźniaczych.
Źródła
- IEEE Spectrum — AI Used to Verify Toughest Mathematics Proof Yet
- Wikipedia — Twin prime conjecture
