AI van Axiom Math verifieert het 246 priemgaptheorema in Lean

Axiom Math zegt dat haar AxiomProver‑systeem een machinaal gecontroleerd Lean 4‑bewijs heeft geproduceerd van het sterkste bekende resultaat over de kieren tussen priemgetallen: de stelling dat er oneindig veel priempaar­en bestaan die niet meer dan 246 van elkaar verschillen. Het bedrijf publiceerde het resultaat op 17 augustus 2026 als een interactieve formalisatie‑blauwdruk, toegeschreven aan 41 genoemde wiskundige, technische en hoofd‑onderzoekers, waarbij IEEE Spectrum meldde het eerst het mijlpaal.

De 246‑grens is de huidige limiet van menselijke kennis in de langdurige aanval op de tweelingpriem‑veronderstelling, de hypothese uit de 19e eeuw dat priemen die precies met twee van elkaar gescheiden zijn, oneindig vaak voorkomen. De projectpagina van Axiom Math beschrijft het werk als een eenduidige formalisatie van James Maynard’s paper uit 2013 “Small gaps between primes” samen met het deel van de Polymath8b‑samenwerking dat Maynard’s grens van 600 verstrakte tot 246. De machinaal gecontroleerde bewijzen zijn georganiseerd in een publieke Lean‑bibliotheek, PrimeGapsLib, waarbij de 246‑stelling het vlaggenschip‑resultaat is.

“Deze stelling vertegenwoordigt momenteel de grens van menselijke kennis over priemgetallen,” zei Ken Ono, de oprichters‑wiskundige van Axiom Math.

Formele verificatie betekent dat een bewijs wordt vertaald naar een taal die een klein, vertrouwd programma, een kernel genaamd, regel voor regel kan controleren. Het resultaat is geen absolute garantie — de bewering zelf moet correct vertaald zijn en de controleur moet betrouwbaar zijn — maar het verwijdert de feilbaarheid van de menselijke scheidsrechter uit de keten. Tot nu toe zijn AI‑systemen die meedoen aan wiskundige benchmarks vooral gemeten op wedstrijdproblemen met korte, zelfstandige bewijzen; de kloof tussen die resultaten en formalisatie op onderzoek‑niveau is groot, een patroon dat zichtbaar is in eerdere systemen die uitblonken in olympische meetkunde terwijl onderzoeksmathematica grotendeels onaangeroerd bleef.

Van 70 miljoen naar 246

De conjectuur zelf, nauwkeurig geformuleerd door Alphonse de Polignac in de 19e eeuw, blijft onbewezen. De eerste eindige grens van welke aard dan ook kwam in 2013, toen Yitang Zhang aantoonde dat er oneindig veel priempaar­en bestaan die binnen 70 miljoen van elkaar liggen. Enkele maanden later introduceerde Maynard een verfijnde zeefmethode en verkleinde de grens tot 600 — werk dat bijdroeg aan zijn Fields‑medaille in 2022 — en de Polymath8b‑samenwerking, waartoe Maynard en Terence Tao behoorden, bracht die naar 246. De blauwdruk van Axiom Math zet die voortgang uiteen als het project dat ze wilden formaliseren.

De formalisatie volgt een pijplijn die het bedrijf in drie fasen beschrijft. Onderzoekers schreven eerst het bewijs als een blauwdruk — elke definitie, lemma en stelling kreeg een label, een precieze formulering en een lijst van de resultaten waarop het gebaseerd is — waardoor een afhankelijkheids­grafiek ontstond die het werk ordende. AxiomProver, het multi‑agent‑systeem van het bedrijf voor wiskundig onderzoek via formeel bewijs, genereerde vervolgens machinaal controleerbare Lean 4‑bewijzen gebouwd op Mathlib, de community‑wiskundebibliotheek, en op PrimeNumberTheoremAnd, het bestaande formalisatieproject onder leiding van Alex Kontorovich en Tao. Het team van Axiom reviewde daarna de gegenereerde code en organiseerde deze in PrimeGapsLib.

De in de bibliotheek opgegeven hoofdresultaten gaan iets verder dan de kop‑stelling. Naast de 246‑grens formaliseert het Maynard’s 600‑grens, en bevat het een zelfstandige verificatie‑uitdaging — gebouwd uitsluitend op Mathlib, met een leeg bewijs‑slot — die iedereen met het Lean‑vergelijkings‑tool in staat stelt onafhankelijk te bevestigen dat de bewijzen in de bibliotheek overeenkomen met de gestelde stellingen. Het bedrijf waarschuwt dat de volledige controle uren kan duren; een gereduceerde versie die de andere twee resultaten dekt, duurt enkele minuten.

Waar dit zich bevindt tussen AI‑formalisatie‑claims

Het resultaat valt in een jaar van toenemende beweringen over AI‑systemen die wiskunde op onderzoeksniveau uitvoeren, waarvan de meeste zijn gebaseerd op wedstrijdscores of korte bewijzen. Axiom Math is een van de meer agressieve claimants: AxiomProver krijgt de eer voor het oplossen van eerder openstaande problemen, inclusief werk dat het bedrijf in peer‑review‑tijdschriften heeft geplaatst, en AI‑systemen hebben nu verschillende langdurige Erdős‑problemen opgelost. De 246‑formalisatie is een ander soort resultaat — geen nieuwe stelling, maar een machinaal gecontroleerde reconstructie van een van de technisch meest veeleisende bewijzen in de moderne getaltheorie.

De meest nabije vergelijking is eerder dit jaar, toen Math, Inc. zijn Gauss‑agent gebruikte om het formele bewijs te voltooien van Maryna Viazovska’s Fields‑medaille‑winnende bol‑verpakkingsresultaten in dimensies 8 en 24. Sidharth Hariharan, de Ph.D.-student aan Carnegie Mellon die de menselijke blauwdruk‑inspanning voor die formalisatie leidde en nu stage loopt bij Axiom Math en een genoemde wiskundige bijdrager is aan het 246‑project, betoogt dat het nieuwe resultaat de meer omvattende prestatie is. Zijn redenering, zoals hij die beschreef, is dat Axiom gebouwd is voor hergebruik: in plaats van een eenmalige formalisatie van één bewijs, is PrimeGapsLib een onderhouden bibliotheek van priem‑gap‑resultaten bedoeld om toekomstig formalisatiewerk en onderzoek te ondersteunen.

Dat onderscheid is van belang voor de interpretatie van het resultaat. Een eenmalige verificatie toont aan dat een systeem een enkel moeilijk bewijs aankan. Een bibliotheek toont iets dat dichter bij infrastructuur ligt — herbruikbare formele gereedschappen waarop andere resultaten kunnen voortbouwen — wat de richting is waarin formele bewijssystemen zich bewegen nu ze overstappen van het oplossen van oefeningen naar het controleren van echte wiskunde. De capaciteitsclaim hier berust op artefacten die publiek en opnieuw uitvoerbaar zijn, in plaats van op een benchmark‑score: de blauwdruk, de Lean‑code en een vergelijkings‑uitdaging ontworpen zodat externe onderzoekers de bewijzen zelf kunnen verifiëren.

Ono plaatst de wiskunde in het kader van een testomgeving voor een grotere ambitie. Als eigenschappen van software — of een programma stopt, of de output correct is voor elke invoer — kunnen worden uitgedrukt als precieze wiskundige beweringen, dan zouden systemen afgeleid van AxiomProver ze formeel kunnen bewijzen, stelt hij, en wijst daarmee op verificatie van AI‑gegenereerde code die infrastructuur, financiën en beveiligingssystemen begint te draaien.

“De wereld staat op het punt te draaien op computercode die niemand heeft gelezen,” zei Ono. “AI is hier en we kunnen niet langer wegkijken — formele bewijsgaring is een testomgeving voor het oplossen van wat ik denk de belangrijkste uitdaging is die we van AI zullen krijgen.”

Voorlopig is het opleverbare product beperkter en controleerbaar: een blauwdruk met 41 auteurs, een publieke Lean‑bibliotheek, en een machinaal geverifieerd bewijs dat priemen die binnen 246 van elkaar liggen nooit opraken — de dichtstbijzijnde geverifieerde buur van de tweelingpriem‑conjectuur, en het diepste stuk onderzoeksmathematica dat een AI‑systeem tot nu toe van begin tot eind heeft gecontroleerd.