Axiom Math’s AI bekræfter 246‑primgap‑teoremet i Lean

Axiom Math siger, at deres AxiomProver‑system har fremstillet et maskintjekket Lean 4‑bevis for det stærkeste kendte resultat om huller mellem primtal: teoremet om, at uendeligt mange primtalspar adskiller sig med højst 246. Virksomheden offentliggjorde resultatet den 17. august 2026 som en interaktiv formaliserings‑blåtryk, der krediterer 41 navngivne matematik‑, ingeniør‑ og hovedforsker‑bidragydere, med IEEE Spectrum først rapporterede milepælen.

Den 246‑grænse udgør i øjeblikket den nuværende kant af menneskelig viden i den lange kamp mod tvilling‑primtals‑formodningen, den 19.‑århundredes hypotese om, at primtal adskilt med præcis to forekommer for evigt. Axiom Math’s projektside beskriver arbejdet som en samlet formalisering af James Maynards 2013‑artikel “Small gaps between primes” sammen med den del af Polymath8b‑samarbejdet, der strammede Maynards grænse fra 600 ned til 246. De maskintjekkede beviser er organiseret i et offentligt Lean‑bibliotek, PrimeGapsLib, hvor 246‑teoremet er hovedresultatet.

„Dette teorem udgør i øjeblikket grænsen for menneskelig viden om primtal,“ sagde Ken Ono, Axiom Math’s grundlæggende matematiker.

Formel verifikation betyder, at et bevis oversættes til et sprog, som et lille, betroet program kaldet en kernel kan kontrollere linje for linje. Resultatet er ikke en absolut garanti – påstanden selv skal oversættes korrekt, og kontrolløren skal være pålidelig – men det fjerner den menneskelige dommers fejlbarlighed fra kæden. Indtil nu har AI‑systemer, der konkurrerer på matematik‑benchmark‑tests, fortrinsvis blevet målt på konkurrence‑opgaver med korte, selvstændige beviser; afstanden mellem disse resultater og formalisering på forskningsniveau har været stor, et mønster der var synligt i tidligere systemer, der udmærkede sig i olympiade‑geometri mens forskningsmatematik stort set blev uberørt.

Fra 70 millioner til 246

Formodningen selv, præcist formuleret af Alphonse de Polignac i det 19. århundrede, forbliver ubevist. Den første endelige grænse af nogen art kom i 2013, da Yitang Zhang beviste, at uendeligt mange primtalspar ligger inden for 70 millioner af hinanden. Månedene efter introducerede Maynard en raffineret sigtemetode og sænkede grænsen til 600 – arbejde der bidrog til hans Fields‑medalje i 2022 – og Polymath8b‑samarbejdet, som omfattede Maynard og Terence Tao, skubbede den ned til 246. Axiom Math’s blåtryk lægger denne progression ud som det projekt, de satte sig for at formalisere.

Formaliseringen følger en pipeline, som virksomheden beskriver i tre faser. Forskere skrev først beviset som en blåtryk – hver definition, lemma og teorem fik en etiket, en præcis formulering og en liste over de resultater, det afhænger af – hvilket skabte en afhængighedsgraf, der sorterede arbejdet. AxiomProver, virksomhedens multi‑agent‑system til matematisk forskning gennem formelle beviser, genererede derefter maskintjekkede Lean 4‑beviser bygget på Mathlib, det fællesskabsbaserede matematikbibliotek, samt på PrimeNumberTheoremAnd, det eksisterende formaliseringsprojekt ledet af Alex Kontorovich og Tao. Axiom‑teamet gennemgik derefter den genererede kode og organiserede den i PrimeGapsLib.

Bibliotekets angivne hovedresultater går lidt ud over hovedteoremet. Ud over 246‑grænsen formaliserer det Maynards 600‑grænse, og det indeholder en selvstændig verifikations‑udfordring – bygget udelukkende på Mathlib, med bevis‑slottet tomt – som gør det muligt for enhver med Lean‑sammenligningsværktøjet at bekræfte uafhængigt, at bibliotekets beviser svarer til de angivne teoremer. Virksomheden advarer om, at den fulde kontrol kan tage timer; en reduceret version, der dækker de to andre resultater, kører på minutter.

Hvor dette placerer sig blandt AI‑formaliserings‑påstande

Resultatet falder i et år med stigende påstande om, at AI‑systemer udfører forsknings‑niveau matematik, de fleste forankret i konkurrence‑score eller korte beviser. Axiom Math har været en af de mere aggressive påståere: AxiomProver krediteres for at have løst tidligere åbne problemer, herunder arbejde som virksomheden har placeret i fagfællebedømte tidsskrifter, og AI‑systemer har nu løst flere langvarige Erdős‑problemer. 246‑formaliseringen er en anden slags resultat – ikke et nyt teorem, men en maskintjekket rekonstruktion af et af de mest teknisk krævende beviser i moderne talteori.

Den nærmeste sammenligning er tidligere i år, da Math, Inc. brugte deres Gauss‑agent til at fuldføre det formelle bevis af Maryna Viazovskas Fields‑medaljevindende kuglepakningsresultater i dimensionerne 8 og 24. Sidharth Hariharan, den Carnegie‑Mellon Ph.D.-studerende, der ledede den menneskelige blåtryk‑indsats på den formalisering og nu er praktikant hos Axiom Math samt navngivet matematisk bidragyder på 246‑projektet, argumenterer for, at det nye resultat er den mere omfattende præstation. Hans begrundelse, som han beskrev, er, at Axiom byggede til genbrug: i stedet for en engangs‑formalisering af et enkelt bevis, er PrimeGapsLib et vedligeholdt bibliotek af prim‑gap‑resultater, beregnet til at støtte fremtidigt formaliseringsarbejde og forskning.

Den sondring er vigtig for, hvordan resultatet skal læses. En engangs‑verifikation viser, at et system kan overleve kontakt med ét svært bevis. Et bibliotek demonstrerer noget, der ligger tættere på infrastruktur – genanvendelig formel maskineri, som andre resultater kan bygge på – hvilket er den retning formelle bevis‑systemer har bevæget sig i, efterhånden som de skifter fra at løse øvelser til at tjekke reel matematik. Påstandens kapacitet hviler her på artefakter, der er offentlige og genkørbare, snarere end på en benchmark‑score: blåtrykket, Lean‑koden og en sammenlignings‑udfordring designet, så eksterne forskere kan verificere beviserne selv.

Ono indrammer matematikken som en testplatform for en større ambition. Hvis egenskaber ved software – om et program terminerer, om dets output er korrekt for hver inddata – kan udtrykkes som præcise matematiske udsagn, så kan systemer afledt af AxiomProver formelt bevise dem, argumenterer han, og peger mod verifikation af AI‑genereret kode, der begynder at køre infrastruktur, finans‑ og sikkerhedssystemer.

„Verden er ved at køre på computerkode, som ingen har læst,“ sagde Ono. „AI er her, og vi kan ikke længere se væk – bevisformalisering er en testplatform for at løse det, jeg mener er den vigtigste udfordring, vi vil stå over for fra AI.“

For nu er leverancen snævrere og tjekbar: en 41‑forfatter‑blåtryk, et offentligt Lean‑bibliotek og et maskintjekket bevis for, at primtal inden for 246 af hinanden aldrig løber ud – tvilling‑primtals‑formodningens nærmeste verificerede nabo, og det dybeste stykke forskningsmatematik, som et AI‑system hidtil har kontrolleret fra ende til anden.