Axiom Math ha completato con il sistema di intelligenza artificiale AxiomProver una dimostrazione formalmente verificata in Lean 4 del risultato attualmente più avanzato sui gap limitati tra numeri primi: esistono infinite coppie di numeri primi la cui distanza non supera 246. Il lavoro non introduce un nuovo teorema matematico, ma ricostruisce e verifica tramite un proof assistant uno dei risultati più complessi della moderna teoria dei numeri, trasformandone definizioni, lemmi e passaggi dimostrativi in codice controllabile automaticamente. La formalizzazione è stata pubblicata il 17 agosto 2026 attraverso un blueprint interattivo attribuito a 41 contributori tra matematici, ingegneri e principal investigator, mentre le dimostrazioni sono raccolte nella libreria pubblica PrimeGapsLib.
Il limite 246 rappresenta il risultato più vicino attualmente disponibile alla congettura dei primi gemelli, secondo la quale esisterebbero infinite coppie di numeri primi separate esattamente da 2. La formulazione più generale del problema dei gap tra primi risale ad Alphonse de Polignac nel XIX secolo, ma la congettura resta tuttora irrisolta. Un primo risultato fondamentale arrivò nel 2013 con Yitang Zhang, che dimostrò l’esistenza di infinite coppie di primi distanti al massimo 70 milioni. Pochi mesi dopo James Maynard sviluppò un metodo di crivello differente che ridusse il limite a 600, un lavoro che contribuì all’assegnazione della Medaglia Fields nel 2022. La collaborazione Polymath8b, alla quale parteciparono tra gli altri Maynard e Terence Tao, riuscì successivamente a portare il limite da 600 a 246. Il progetto di Axiom Math riunisce in un’unica formalizzazione il lavoro pubblicato da Maynard nel 2013, Small gaps between primes, e la parte del successivo progetto Polymath8b necessaria per ottenere il limite attuale.
La formalizzazione è stata organizzata attraverso una procedura in tre fasi. Nella prima, i ricercatori hanno trasformato la dimostrazione matematica in un blueprint strutturato, assegnando a ogni definizione, lemma e teorema un identificatore, un enunciato preciso e l’elenco dei risultati dai quali dipende. Questa struttura ha prodotto un grafo delle dipendenze che stabilisce l’ordine nel quale devono essere costruiti e verificati i diversi elementi della dimostrazione. Nella fase successiva AxiomProver, sistema multi-agente sviluppato da Axiom Math per la ricerca matematica attraverso prove formali, ha generato le dimostrazioni verificabili automaticamente in Lean 4. Il codice utilizza Mathlib, la principale libreria matematica della comunità Lean, e PrimeNumberTheoremAnd, un progetto di formalizzazione già esistente guidato da Alex Kontorovich e Terence Tao. Il team di Axiom Math ha infine revisionato il codice prodotto e lo ha organizzato all’interno di PrimeGapsLib.
La libreria non contiene soltanto la dimostrazione relativa al limite 246. PrimeGapsLib formalizza anche il precedente risultato di Maynard con limite 600 e mette a disposizione una procedura indipendente per verificare che le dimostrazioni contenute nella libreria corrispondano effettivamente ai teoremi dichiarati. La verifica è costruita esclusivamente sopra Mathlib e lascia vuoto lo spazio destinato alla dimostrazione, permettendo di utilizzare il comparator tool di Lean per confrontare autonomamente i risultati. La verifica completa relativa al teorema con limite 246 può richiedere diverse ore, mentre una versione ridotta che controlla gli altri due risultati previsti dal progetto può essere eseguita in pochi minuti.
La caratteristica centrale del risultato è proprio il ricorso alla verifica formale. Una dimostrazione matematica viene tradotta in una rappresentazione che il kernel di Lean può controllare passaggio per passaggio, verificando che ciascuna inferenza segua dalle definizioni, dagli assiomi e dai risultati precedentemente dimostrati. Questo tipo di controllo non costituisce una garanzia assoluta indipendente da ogni presupposto, perché l’enunciato matematico deve essere tradotto correttamente nel linguaggio formale e il kernel utilizzato per verificarlo deve essere affidabile, ma elimina dalla verifica della catena logica la possibilità che un revisore umano non individui un errore presente in uno dei numerosi passaggi della dimostrazione.
Il progetto si distingue inoltre dai risultati ottenuti da molti sistemi di intelligenza artificiale valutati attraverso benchmark matematici composti da problemi olimpici o dimostrazioni relativamente brevi e autosufficienti. In questo caso il sistema ha lavorato sulla ricostruzione completa di matematica di livello di ricerca già esistente. AxiomProver è stato utilizzato anche per affrontare problemi precedentemente aperti, compresi risultati che Axiom Math ha successivamente portato in pubblicazioni peer-reviewed, mentre altri sistemi di intelligenza artificiale hanno recentemente contribuito alla soluzione di diversi problemi di Erdős rimasti aperti per lungo tempo. La formalizzazione del limite 246 ha tuttavia una natura differente: il risultato matematico era già noto, mentre l’obiettivo consisteva nel trasformare l’intera costruzione in una prova controllabile da una macchina.
Un precedente comparabile riguarda la formalizzazione dei risultati di Maryna Viazovska sul sphere packing nelle dimensioni 8 e 24, lavoro per il quale la matematica ucraina ha ricevuto la Medaglia Fields. Nel corso del 2026 Math, Inc. ha utilizzato il proprio agente Gauss per completarne la dimostrazione formale. Sidharth Hariharan, dottorando alla Carnegie Mellon University che aveva guidato il lavoro umano sul blueprint di quella formalizzazione e che successivamente è entrato come intern in Axiom Math partecipando anche al progetto sui prime gap, considera però PrimeGapsLib un risultato più esteso sotto il profilo dell’infrastruttura costruita. La differenza consiste nel fatto che il progetto non è stato organizzato come una verifica isolata di una singola dimostrazione, ma come una libreria mantenuta e riutilizzabile dedicata ai risultati sui gap tra numeri primi, sulla quale potranno essere costruite ulteriori formalizzazioni.
Gli elementi necessari per verificare il risultato sono stati resi pubblici e rieseguibili: il blueprint descrive la struttura matematica e le dipendenze tra i risultati, PrimeGapsLib contiene il codice Lean e il challenge basato sul comparator permette a ricercatori esterni di verificare indipendentemente la corrispondenza tra le prove e gli enunciati dichiarati. Ken Ono, founding mathematician di Axiom Math, ha indicato proprio questo tipo di formalizzazione come banco di prova anche per applicazioni successive alla verifica del software. Proprietà come la terminazione di un programma o la correttezza del suo output per tutti gli input possono infatti essere espresse, quando possibile, attraverso enunciati matematici precisi e sottoposte allo stesso principio di dimostrazione formale, con possibili applicazioni alla verifica del codice generato dall’intelligenza artificiale destinato a infrastrutture, sistemi finanziari e applicazioni di sicurezza.
Il risultato concreto del progetto resta la costruzione di un blueprint con 41 contributori, di una libreria Lean pubblica e di una dimostrazione verificata automaticamente dell’esistenza di infinite coppie di numeri primi distanti non più di 246. La congettura dei primi gemelli, che richiederebbe di ridurre quella distanza esattamente a 2, rimane aperta, mentre il limite 246 continua a rappresentare il più avanzato risultato dimostrato in questa direzione.
Questo articolo è stato redatto con il supporto di strumenti di intelligenza artificiale (AI)