AI společnosti Axiom Math ověřuje teorém o 246 mezích mezi prvočísly v Lean

Axiom Math uvádí, že jeho systém AxiomProver vytvořil strojově ověřený důkaz v Lean 4 na nejsilnější známý výsledek o mezerách mezi prvočísly: teorém, že existuje nekonečně mnoho dvojic prvočísel, jejichž rozdíl nepřesahuje 246. Společnost výsledek publikovala 17. srpna 2026 jako interaktivní formalizační návod připsaný 41 pojmenovaným přispěvatelům z oblasti matematiky, inženýrství a hlavních vyšetřovatelů, přičemž IEEE Spectrum poprvé informoval o tomto milníku.

Hodnota 246 představuje současný okraj lidského poznání v dlouhém úsilí o dvojčinnou hypotézu, 19. století formulovanou hypotézu, že prvočísla oddělená právě dvěma se opakují donekonečna. Stránka projektu Axiom Math popisuje práci jako jednotnou formalizaci článku Jamese Maynarda z roku 2013 „Small gaps between primes“ spolu s částí následného projektu Polymath8b, která zpřesnila Maynardovu mez 600 na 246. Strojově ověřené důkazy jsou uspořádány v veřejné knihovně Lean, PrimeGapsLib, přičemž teorém 246 je jejím hlavním výsledkem.

„Tento teorém v současnosti představuje hranici lidského poznání o prvočíslech,“ řekl Ken Ono, zakladatel matematiků ve společnosti Axiom Math.

Formální verifikace znamená převést důkaz do jazyka, který malý, důvěryhodný program nazývaný jádro dokáže kontrolovat řádek po řádku. Výsledek není absolutní zárukou — výrok sám musí být správně přeložen a kontrolor musí být spolehlivý — ale odstraňuje lidskou chybovatelnost z řetězce. Doposud byly AI systémy soutěžící v matematických benchmarkech měřeny převážně na soutěžních úlohách s krátkými, samostatnými důkazy; mezera mezi těmito výsledky a formalizací na úrovni výzkumu byla velká, což je patrné u dřívějších systémů, které vynikaly v olympijské geometrii, zatímco výzkumnou matematiku zůstaly téměř nedotčeny.

Od 70 milionů k 246

Samotná conjectura, přesně formulovaná Alphonsem de Polignacem v 19. století, zůstává neprokázaná. První konečná mez jakéhokoli druhu se objevila v roce 2013, kdy Yitang Zhang dokázal, že nekonečně mnoho dvojic prvočísel leží v rozmezí 70 milionů. O několik měsíců později Maynard představil vylepšenou síťovou metodu a snížil mez na 600 — práce, která přispěla k jeho Fieldsově medaili v roce 2022 — a spolupráce Polymath8b, zahrnujícího Maynarda a Terenceho Tao, ji posunula na 246. Návrh Axiom Math představuje tento vývoj jako projekt, který chtěl formalizovat.

Formalizace následuje postup, který společnost popisuje ve třech fázích. Výzkumníci nejprve napsali důkaz jako návod — každá definice, lemma a teorém dostaly štítek, přesné znění a seznam výsledků, na nichž závisejí — čímž vznikl graf závislostí uspořádávající práci. AxiomProver, víceagentní systém společnosti pro matematický výzkum prostřednictvím formálního důkazu, následně vygeneroval strojově kontrolovatelné důkazy v Lean 4 postavené na Mathlib, komunitní matematické knihovně, a na PrimeNumberTheoremAnd, existujícím formalizačním projektu vedeném Alexem Kontorovichem a Tao. Tým Axiom poté přezkoumal vygenerovaný kód a uspořádal jej do PrimeGapsLib.

Hlavní výsledky knihovny uvádějí mírně více než samotný hlavní teorém. K hodnotě 246 zároveň formalizuje Maynardovu mez 600 a obsahuje samostatnou výzvu k ověření — postavenou výhradně na Mathlib, s prázdným místem pro důkaz — která umožňuje komukoli s nástrojem Lean comparator nezávisle potvrdit, že důkazy knihovny odpovídají uvedeným teorémům. Společnost varuje, že úplná kontrola může trvat hodiny; zkrácená verze pokrývající další dva výsledky běží během několika minut.

Kde to stojí mezi tvrzeními o AI formalizaci

Výsledek spadá do roku, kdy se zvyšuje počet tvrzení o tom, že AI systémy provádějí výzkumnou matematiku, přičemž většina z nich je podložena soutěžními skóre nebo krátkými důkazy. Axiom Math patří mezi nejagresivnější tvrditele: AxiomProver je přičítán k řešení dříve otevřených problémů, včetně prací, které společnost publikovala v recenzovaných časopisech, a AI systémy nyní vyřešily několik dlouhodobých Erdősových problémů. Formalizace 246 je jiného druhu výsledek — ne nový teorém, ale strojově ověřená rekonstrukce jednoho z nejnáročnějších důkazů moderní teorie čísel.

Nejbližší srovnání je z počátku tohoto roku, kdy Math, Inc. použil svého agenta Gauss k dokončení formálního důkazu výsledků o balení koulí v dimenzích 8 a 24, které získaly Fieldsovu medailu pro Marynu Viazovskou. Sidharth Hariharan, doktorand Carnegie Mellon, který vedl lidský návodový tým na této formalizaci a nyní působí jako stážista ve společnosti Axiom Math a je pojmenovaným matematickým přispěvatelem projektu 246, tvrdí, že nový výsledek je komplexnější úspěch. Jeho argumentace, jak sám popsal, spočívá v tom, že Axiom byl vytvořen pro opakované použití: místo jednorázové formalizace jediného důkazu je PrimeGapsLib udržovanou knihovnou výsledků o mezerách mezi prvočísly, určenou k podpoře budoucí práce a výzkumu v oblasti formalizace.

Toto rozlišení má vliv na to, jak by měl být výsledek interpretován. Jednorázové ověření ukazuje, že systém dokáže zvládnout jeden obtížný důkaz. Knihovna ukazuje něco blíže infrastruktuře — znovupoužitelný formální aparát, na který mohou stavět další výsledky — což je směr, kterým se formální důkazové systémy ubírají, když přecházejí od řešení cvičení k ověřování skutečné matematiky. Nárok na schopnost zde spočívá v artefaktech, které jsou veřejné a opakovatelně spustitelné, nikoli v benchmarkovém skóre: návod, kód v Lean a výzva k porovnání navržená tak, aby externí výzkumníci mohli důkazy ověřit sami.

Ono představuje matematiku jako testovací prostředí pro větší ambice. Pokud lze vlastnosti softwaru — zda program končí, zda je jeho výstup správný pro každý vstup — vyjádřit jako přesné matematické tvrzení, pak systémy odvozené od AxiomProveru by je mohly formálně dokázat, argumentuje, což směřuje k verifikaci AI‑generovaného kódu, který začíná provozovat infrastrukturu, finance a bezpečnostní systémy.

„Svět se chystá fungovat na počítačovém kódu, který nikdo nečetl,“ řekl Ono. „AI je zde a už nemůžeme odvrátit zrak — formalizace důkazů je testovací prostředí pro řešení toho, co považuji za nejdůležitější výzvu, které budeme čelit od AI.“

Prozatím je výstup užší a ověřitelný: návod od 41 autorů, veřejná knihovna Lean a strojově ověřený důkaz, že prvočísla v rozmezí 246 nikdy nevyčerpají — nejbližší ověřený soused dvojčinné conjectury a nejhlubší část výzkumné matematiky, kterou AI systém doposud kompletně ověřil od začátku do konce.