Axiom Maths AI verifiserer 246‑primgap‑teoremet i Lean

Axiom Math sier at deres AxiomProver‑system har produsert et maskinsjekket Lean 4‑bevis på det sterkeste kjente resultatet om hull mellom primtall: teoremet om at uendelig mange primtallpar skiller seg med høyst 246. Selskapet publiserte resultatet 17. august 2026 som en interaktiv formaliserings‑blåkopi kreditert til 41 navngitte matematiske, tekniske og hoved‑undersøkelsesbidragsytere, med IEEE Spectrum først rapporterte milepælen.

Grensen på 246 er den nåværende grensen for menneskelig kunnskap i den langvarige angrepet på tvillingprimtall‑hypotesen, den 1800‑talls hypotesen om at primtall separert med nøyaktig to forekommer for alltid. Axiom Maths prosjekt‑side beskriver arbeidet som en samlet formalisering av James Maynards 2013‑artikkel «Small gaps between primes» sammen med delen av Polymath8b‑samarbeidets oppfølging som strammet Maynards grense fra 600 ned til 246. De maskinsjekkede bevisene er organisert i et offentlig Lean‑bibliotek, PrimeGapsLib, med 246‑teoremet som hovedresultat.

«Dette teoremet representerer for øyeblikket terskelen for menneskelig kunnskap om primtall,» sa Ken Ono, Axiom Maths grunnlegger‑matematiker.

Formell verifisering betyr å oversette et bevis til et språk som et lite, pålitelig program kalt en kjerne kan sjekke linje for linje. Resultatet er ingen absolutt garanti – påstanden må selv oversettes korrekt, og sjekkerprogrammet må være pålitelig – men det fjerner den menneskelige dommerens feilbarlighet fra kjeden. Fram til nå har AI‑systemer som konkurrerer på matematiske benchmark‑tester hovedsakelig blitt målt på konkurranseoppgaver med korte, selvstendige bevis; gapet mellom disse resultatene og formalisering på forskningsnivå har vært stort, et mønster som var synlig i tidligere systemer som utmerket seg i olympiade‑geometri.

Fra 70 millioner til 246

Selve formodningen, nøyaktig formulert av Alphonse de Polignac på 1800‑tallet, er fortsatt ubevist. Den første endelige grensen av noe slag kom i 2013, da Yitang Zhang beviste at uendelig mange primtallpar ligger innen 70 millioner av hverandre. Månedene etter introduserte Maynard en raffinert silmetode og reduserte grensen til 600 – arbeid som bidro til hans Fields‑medalje i 2022 – og Polymath8b‑samarbeidet, som inkluderte Maynard og Terence Tao, presset den ned til 246. Axiom Maths blåkopi legger frem denne utviklingen som prosjektet den ønsket å formalisere.

Formaliseringen følger en arbeidsflyt som selskapet beskriver i tre faser. Forskerne skrev først beviset som en blåkopi – hver definisjon, lemma og teorem fikk en etikett, en presis påstand og en liste over resultatene den avhenger av – og produserte en avhengighetsgraf som organiserte arbeidet. AxiomProver, selskapets multi‑agent‑system for matematisk forskning gjennom formelle bevis, genererte deretter maskinsjekkbare Lean 4‑bevis bygget på Mathlib, fellesskapets matematikkbibliotek, og på PrimeNumberTheoremAnd, det eksisterende formaliseringsprosjektet ledet av Alex Kontorovich og Tao. Axiom‑teamet gjennomgikk så den genererte koden og organiserte den i PrimeGapsLib.

Bibliotekets oppgitte hovedresultater går litt utover hovedteoremet. Ved siden av 246‑grensen formalisere den Maynards 600‑grense, og den inkluderer en selvstendig verifiserings‑utfordring – bygget kun på Mathlib, med bevisplassen stående tom – som lar alle med Lean‑sammenligningsverktøyet uavhengig bekrefte at bibliotekets bevis samsvarer med de oppgitte teoremene. Selskapet advarer om at full sjekk kan ta timer; en redusert versjon som dekker de to andre resultatene tar minutter.

Hvor dette står blant påstander om AI‑formalisering

Resultatet kommer i et år med økende påstander om at AI‑systemer utfører forskningsnivå‑matematikk, de fleste forankret i konkurransescore eller korte bevis. Axiom Math har vært en av de mest aggressive pådriverne: AxiomProver får kreditt for å ha løst tidligere åpne problemer, inkludert arbeid selskapet har publisert i fagfellevurderte tidsskrifter, og AI‑systemer har nå løst flere langvarige Erdős‑problemer. 246‑formaliseringen er en annen type resultat – ikke et nytt teorem, men en maskinsjekket rekonstruksjon av ett av de mest teknisk krevende bevisene i moderne tallteori.

Den nærmeste sammenligningen er tidligere i år, da Math, Inc. brukte sin Gauss‑agent til å fullføre det formelle beviset av Maryna Viazovskas Fields‑medaljevinnende kulepakningsresultater i dimensjonene 8 og 24. Sidharth Hariharan, Ph.D.-student ved Carnegie Mellon som ledet den menneskelige blåkopi‑innsatsen på den formaliseringen og nå er praktikant hos Axiom Math og navngitt matematisk bidragsyter på 246‑prosjektet, hevder at det nye resultatet er den mer omfattende prestasjonen. Hans begrunnelse, som han beskrev, er at Axiom er bygget for gjenbruk: i stedet for en engangs‑formalisering av ett enkelt bevis, er PrimeGapsLib et vedlikeholdt bibliotek med primhull‑resultater ment å støtte fremtidig formaliseringsarbeid og forskning.

Den distinksjonen er viktig for hvordan resultatet skal forstås. En engangs‑verifisering viser at et system kan håndtere ett vanskelig bevis. Et bibliotek viser noe som ligner infrastruktur – gjenbrukbar formell maskineri som andre resultater kan bygge på – noe som er retningen formelle bevis‑systemer har tatt mens de går fra å løse oppgaver til å sjekke ekte matematikk. Påstandene om kapasitet her hviler på artefakter som er offentlige og kan kjøres på nytt, snarere enn på en benchmark‑score: blåkopien, Lean‑koden og en sammenligningsutfordring designet slik at eksterne forskere kan verifisere bevisene selv.

Ono rammer inn matematikken som en testbenk for en større ambisjon. Hvis egenskaper ved programvare – om et program terminerer, om output er korrekt for alle input – kan uttrykkes som presise matematiske påstander, så kan systemer avledet fra AxiomProver formelt bevise dem, hevder han, og peker mot verifisering av AI‑generert kode som begynner å kjøre infrastruktur-, finans- og sikkerhetssystemer.

«Verden er i ferd med å kjøre på datakode som ingen har lest,» sa Ono. «AI er her, og vi kan ikke lenger se bort – formalisering av bevis er en testbenk for å løse det jeg mener er den viktigste utfordringen vi vil møte fra AI.»

Foreløpig er leveransen smalere og sjekkbar: en blåkopi med 41 forfattere, et offentlig Lean‑bibliotek, og et maskin‑verifisert bevis på at primtall innen 246 av hverandre aldri tar slutt – tvillingprimtall‑hypotesens nærmeste verifiserte nabo, og det dypeste forskningsmatematiske arbeidet et AI‑system hittil har sjekket fra ende til ende.