L’IA di Axiom Math verifica il teorema dei 246 gap tra numeri primi in Lean

Axiom Math afferma che il suo sistema AxiomProver ha prodotto una dimostrazione in Lean 4 verificata da macchina del risultato più forte finora noto sui gap tra numeri primi: il teorema secondo cui infiniti coppie di primi differiscono di non più di 246. L’azienda ha pubblicato il risultato il 17 agosto 2026 come una blueprint di formalizzazione interattiva attribuita a 41 contributori nominati, tra matematici, ingegneri e investigatori principali, con IEEE Spectrum che ha riportato per prima la pietra miliare.

Il limite di 246 rappresenta l’attuale frontiera della conoscenza umana nella lunga battaglia contro la congettura dei gemelli primi, l’ipotesi del XIX secolo secondo cui i primi separati esattamente di due ricorrono all’infinito. La pagina del progetto di Axiom Math descrive il lavoro come una formalizzazione unificata del documento del 2013 di James Maynard “Small gaps between primes” insieme alla parte del seguito della collaborazione Polymath8b che ha ridotto il limite di Maynard da 600 a 246. Le dimostrazioni verificate da macchina sono organizzate in una libreria pubblica Lean, PrimeGapsLib, con il teorema 246 come risultato di punta.

“Questo teorema rappresenta attualmente la soglia della conoscenza umana sui numeri primi”, ha detto Ken Ono, matematico fondatore di Axiom Math.

La verifica formale consiste nel tradurre una dimostrazione in un linguaggio che un piccolo programma affidabile, chiamato kernel, può controllare riga per riga. Il risultato non è una garanzia assoluta — l’enunciato stesso deve essere tradotto correttamente e il verificatore deve essere solido — ma elimina la fallibilità del revisore umano dalla catena. Finora, i sistemi di IA che competono nei benchmark di matematica sono stati per lo più valutati su problemi di gara con dimostrazioni brevi e autonome; il divario tra tali risultati e la formalizzazione a livello di ricerca è stato ampio, un modello visibile in sistemi precedenti che eccellevano nella geometria olimpica lasciando in gran parte intatta la matematica di ricerca.

Da 70 milioni a 246

La congettura stessa, formulata con precisione da Alphonse de Polignac nel XIX secolo, rimane non dimostrata. Il primo limite finito di qualsiasi tipo arrivò nel 2013, quando Yitang Zhang dimostrò che infiniti coppie di primi si trovano entro 70 milioni l’una dall’altra. Pochi mesi dopo, Maynard introdusse un metodo di crivello raffinato e ridusse il limite a 600 — lavoro che contribuì alla sua Medaglia Fields del 2022 — e la collaborazione Polymath8b, che includeva Maynard e Terence Tao, lo portò a 246. La blueprint di Axiom Math espone questa progressione come il progetto che si proponeva di formalizzare.

La formalizzazione segue una pipeline descritta dall’azienda in tre fasi. I ricercatori hanno prima scritto la dimostrazione come una blueprint — ogni definizione, lemma e teorema dotati di un’etichetta, di un enunciato preciso e di un elenco dei risultati da cui dipendono — producendo un grafo di dipendenze che ordinava il lavoro. AxiomProver, il sistema multi‑agente dell’azienda per la ricerca matematica tramite dimostrazioni formali, ha poi generato dimostrazioni Lean 4 verificabili da macchina basate su Mathlib, la libreria matematica della comunità, e su PrimeNumberTheoremAnd, il progetto di formalizzazione esistente guidato da Alex Kontorovich e Tao. Il team di Axiom ha quindi revisionato il codice generato e lo ha organizzato in PrimeGapsLib.

I risultati principali dichiarati dalla libreria vanno leggermente oltre il teorema principale. Oltre al limite di 246, formalizza il limite di 600 di Maynard e include una sfida di verifica autonoma — costruita esclusivamente su Mathlib, con lo spazio della dimostrazione lasciato vuoto — che consente a chiunque disponga dello strumento di confronto Lean di confermare in modo indipendente che le dimostrazioni della libreria corrispondono ai teoremi dichiarati. L’azienda avverte che il controllo completo può richiedere ore; una versione ridotta che copre gli altri due risultati viene eseguita in pochi minuti.

Dove si colloca questo tra le affermazioni di formalizzazione IA

Il risultato si colloca in un anno di affermazioni crescenti sui sistemi IA che svolgono matematica di livello di ricerca, la maggior parte delle quali ancorate a punteggi di competizione o a dimostrazioni brevi. Axiom Math è stato uno dei più aggressivi sostenitori: AxiomProver è accreditato per aver risolto problemi precedentemente aperti, inclusi lavori che l’azienda ha pubblicato su riviste peer‑reviewed, e i sistemi IA hanno ora risolto diversi problemi di Erdős di lunga data. La formalizzazione del 246 è un tipo diverso di risultato — non un nuovo teorema, ma una ricostruzione verificata da macchina di una delle dimostrazioni più tecnicamente impegnative nella teoria dei numeri moderna.

Il confronto più vicino è stato all’inizio di quest’anno, quando Math, Inc. ha utilizzato il suo agente Gauss per completare la dimostrazione formale dei risultati di packing sferico vincitori della Medaglia Fields di Maryna Viazovska nelle dimensioni 8 e 24. Sidharth Hariharan, dottorando della Carnegie Mellon che ha guidato lo sforzo umano della blueprint su quella formalizzazione e ora stagista presso Axiom Math e contribuente matematico nominato nel progetto 246, sostiene che il nuovo risultato sia l’impresa più completa. Il suo ragionamento, come ha descritto, è che Axiom è stato costruito per il riuso: piuttosto che una formalizzazione una tantum di una singola dimostrazione, PrimeGapsLib è una libreria mantenuta di risultati sui gap tra primi destinata a supportare futuri lavori di formalizzazione e ricerca.

Questa distinzione è importante per l’interpretazione del risultato. Una verifica una tantum dimostra che un sistema può affrontare una dimostrazione difficile. Una libreria dimostra qualcosa di più simile a un’infrastruttura — una macchina formale riutilizzabile su cui altri risultati possono basarsi — che è la direzione verso cui i sistemi di dimostrazione formale si stanno muovendo mentre passano dal risolvere esercizi al verificare matematica reale. L’affermazione di capacità qui si basa su artefatti pubblici e rieseguibili piuttosto che su un punteggio di benchmark: la blueprint, il codice Lean e una sfida di confronto progettata affinché ricercatori esterni possano verificare le dimostrazioni autonomamente.

Ono inquadra la matematica come banco di prova per un’ambizione più ampia. Se le proprietà del software — ad esempio se un programma termina, se il suo output è corretto per ogni input — possono essere espresse come enunciati matematici precisi, allora i sistemi derivati da AxiomProver potrebbero dimostrarle formalmente, sostiene, indicando una verifica del codice generato dall’IA che inizia a gestire infrastrutture, finanza e sistemi di sicurezza.

“Il mondo sta per funzionare su codice informatico che nessuno ha letto”, ha detto Ono. “L’IA è qui e non possiamo più distogliere lo sguardo — la formalizzazione delle dimostrazioni è un banco di prova per risolvere quella che, a mio avviso, è la sfida più importante che dovremo affrontare dall’IA.”

Per ora il risultato è più limitato e verificabile: una blueprint di 41 autori, una libreria Lean pubblica e una dimostrazione verificata da macchina che i primi entro 246 l’uno dall’altro non si esauriscono mai — il vicino verificato più prossimo della congettura dei gemelli primi, e il risultato di ricerca matematica più profondo che un sistema IA abbia finora controllato dall’inizio alla fine.