A formal proof of the Ramanujan--Nagell theorem in Lean 4

Questo articolo presenta una formalizzazione completa in Lean 4 del teorema di Ramanujan-Nagell, che identifica le uniche soluzioni intere dell'equazione diofantea $x^2 + 7 = 2^n$, includendo la verifica delle dipendenze algebriche necessarie e analizzando le sfide nel tradurre le dimostrazioni matematiche tradizionali in un contesto di verifica formale.

L'essenziale

Il Mistero del Numero 7: Come un Computer ha Risolto un Enigma di Ramanujan

Immagina di avere un'enorme libreria di matematica, piena di libri scritti da geni come Ramanujan. In uno di questi libri, c'è un indovinello scritto nel 1913: "Per quali numeri $n$, se prendi $2^n$ e togli 7, ottieni un quadrato perfetto?"

Ramanujan aveva già trovato alcune risposte (come 3, 4, 5, 7 e 15), ma si chiedeva: "Esistono altre risposte nascoste? O queste sono le uniche?"
Per decenni, i matematici umani hanno provato a risolvere questo enigma. Nel 1948, un matematico di nome Nagell ha finalmente dimostrato che sì, quelle sono le uniche soluzioni. Ma la sua prova era scritta su carta, con passaggi che un essere umano può seguire ma che sono difficili da controllare al 100% senza errori.

Questo articolo racconta come un gruppo di ricercatori abbia usato un computer super-intelligente (chiamato Lean 4) per riscrivere quella prova, riga per riga, costringendo il computer a verificare ogni singolo passaggio. Il risultato? Una prova matematica che non può avere dubbi: è verificata al 100%.

L'Analogia della Costruzione: Non solo i Mattoni, ma anche le Fondamenta

Per costruire questa prova digitale, gli autori non hanno potuto semplicemente dire "costruiamo la casa". Hanno dovuto costruire prima l'intero quartiere. Ecco come funziona, usando metafore:

1. Il Laboratorio Chimico (La Teoria dei Numeri)

Immagina che i numeri siano come atomi. In alcuni mondi magici (chiamati "campi quadratici"), gli atomi si comportano in modo strano. Per risolvere l'enigma di Ramanujan, i matematici devono entrare in un mondo speciale chiamato $\mathbb{Q}(\sqrt{-7})$.
In questo mondo, i numeri non sono solo 1, 2, 3... ma includono cose strane come $\frac{1+\sqrt{-7}}{2}$.

• La sfida: Nel libro di testo, si dà per scontato che questo mondo funzioni bene (che ogni numero si possa scomporre in "atomi" unici, come i numeri primi).
• Nel computer: Il computer non crede a nulla finché non lo vedi. Gli autori hanno dovuto scrivere codice per costruire questo mondo da zero, dimostrando al computer che le sue regole sono solide, che non ci sono buchi e che le "atomi" (i numeri primi di quel mondo) si comportano come previsto. È come dover costruire le fondamenta di un grattacielo prima di poter mettere il primo mattone.

2. Il Traduttore di Lingue (Isomorfismi)

C'è un problema divertente: in matematica, lo stesso mondo può essere descritto in due modi diversi.

• Modo A: "Usiamo la radice di -7".
• Modo B: "Usiamo la radice di -7 divisa per 2 più 1".
  Per un umano, è ovvio che sono la stessa cosa. Per un computer, sono due lingue completamente diverse.
  Gli autori hanno dovuto scrivere un traduttore (un isomorfismo) che collegasse queste due versioni, permettendo al computer di saltare da una all'altra senza andare in tilt. È come se avessero dovuto costruire un ponte tra due isole che sembravano diverse, ma erano in realtà la stessa isola vista da angolazioni diverse.

3. L'Investigatore Privato (La Prova)

Una volta costruita la "città" dei numeri, l'investigatore (il teorema) entra in azione.

• Il caso: "Chi ha commesso il crimine? Chi è il numero $n$ che fa $x^2 + 7 = 2^n$?"
• La strategia: L'investigatore divide il caso in due:
  1. Il caso "Pari": Se il numero è pari, è facile. Il computer controlla e trova subito la soluzione.
  2. Il caso "Dispari": Qui diventa complicato. L'investigatore usa una "lente d'ingrandimento" (la teoria dei numeri) per vedere che il numero deve essere uno di tre tipi specifici.
• Il colpo di scena: Usando una formula magica (lo sviluppo binomiale), l'investigatore riduce i sospetti a soli tre gruppi. Poi, usa un trucco matematico (valutazione $p$-adica, che è come contare quante volte un numero è divisibile per 7) per dimostrare che non può esserci più di un colpevole per ogni gruppo.
• Il verdetto: Alla fine, il computer controlla a mano i pochi casi rimasti e conferma: "Sì, i colpevoli sono solo quelli che Ramanujan aveva già trovato".

Perché è così difficile? (Le Sfide)

Il paper spiega che scrivere queste prove per un computer è molto più faticoso che scriverle su carta. Ecco perché:

• Niente "Fai per finta": Su carta, un matematico può dire "è ovvio che...". Il computer risponde: "Dimostramelo". Ogni piccolo passaggio, anche quello che sembra banale, deve essere scritto esplicitamente.
• I "Diamanti" dei Tipi: Immagina di avere due chiavi che aprono la stessa porta. Per un umano sono la stessa chiave. Per il computer, sono due chiavi diverse e se provi ad usarle insieme senza dirgli che sono uguali, si blocca. Gli autori hanno passato ore a "lucidare" queste chiavi per farle combaciare perfettamente.
• L'AI come Assistente: Una parte interessante del paper è l'uso dell'Intelligenza Artificiale. Gli autori hanno usato un'AI (come un assistente molto veloce) che suggeriva i prossimi passi, correggeva gli errori di sintassi e trovava le formule giuste nei libri di testo digitali. È stato come avere un tutor personale che ti aiuta a non impantanarti nei dettagli noiosi, permettendoti di concentrarti sulla logica.

Conclusione: Cosa ci insegna?

Questo lavoro non è solo una vittoria per la matematica, ma un passo avanti per il futuro. Dimostra che:

1. Possiamo usare i computer per verificare le prove matematiche più complesse, eliminando il rischio di errori umani.
2. L'Intelligenza Artificiale sta diventando un partner fondamentale per i matematici, aiutandoli a costruire queste "cattedrali digitali" molto più velocemente.
3. La matematica di Ramanujan, nata quasi 110 anni fa, è stata finalmente "congelata" in una forma eterna e inattaccabile grazie al codice.

In sintesi: Hanno preso un indovinello vecchio di un secolo, costruito un laboratorio matematico digitale per risolverlo, e hanno usato un assistente robot per assicurarsi che non ci fosse nemmeno un errore di battitura. Il risultato è una certezza assoluta che, per la formula $x^2 + 7 = 2^n$, non ci sono altri segreti nascosti.

Sommario tecnico

1. Il Problema

Il teorema di Ramanujan–Nagell è un'equazione diofantea esponenziale che chiede di trovare tutte le soluzioni intere $(n, x)$ per l'equazione:
$$x^2 + 7 = 2^n$$
Ramanujan, nel 1913, ipotizzò che le uniche soluzioni corrispondessero ai valori $n \in \{3, 4, 5, 7, 15\}$ (con i corrispondenti $x$). Questa congettura fu dimostrata da Trygve Nagell nel 1948.
L'obiettivo del paper è fornire la prima formalizzazione completa e verificata da macchina di questa congettura di Ramanujan all'interno di un assistente di dimostrazione, specificamente utilizzando Lean 4 e la libreria Mathlib.

2. Metodologia e Architettura

La formalizzazione è stata realizzata in Lean 4, suddivisa in cinque file principali che coprono circa 3.570 righe di codice e 125 dichiarazioni (definizioni, lemmi, teoremi). L'approccio segue la dimostrazione classica di Stewart e Tall, ma richiede un'elaborazione significativa per gestire le complessità della teoria algebrica dei numeri in un contesto formale.

L'architettura si divide in due livelli:

1. Infrastruttura di Teoria Algebrica dei Numeri: File dedicati alla definizione e alle proprietà dell'anello degli interi del campo quadratico $K = \mathbb{Q}(\sqrt{-7})$.
2. Dimostrazione Specifica: La logica matematica che risolve l'equazione diofantea.

Componenti Chiave dell'Infrastruttura

• Identificazione dell'Anello degli Interi ($O_K$): Poiché $-7 \equiv 1 \pmod 4$, l'anello degli interi non è $\mathbb{Z}[\sqrt{-7}]$, ma $\mathbb{Z}[\frac{1+\sqrt{-7}}{2}]$. La formalizzazione deve gestire due diverse presentazioni del campo quadratico in Mathlib (una con generatore $\sqrt{-7}$ e l'altra con $\frac{1+\sqrt{-7}}{2}$) e costruire un isomorfismo esplicito tra di esse per trasportare le proprietà di chiusura integrale.
• Proprietà Algebriche: Viene dimostrato che $O_K$ è un Dominio a Fattorizzazione Unica (UFD) e un Dominio a Ideali Principali (PID). Questo si basa sul calcolo del discriminante ($-7$) e sull'applicazione del limite di Minkowski per mostrare che il numero di classi è 1.
• Gruppo delle Unità: Viene dimostrato che le uniche unità in $O_K$ sono $\pm 1$. Questo richiede l'uso del Teorema delle Unità di Dirichlet e un'analisi dei radici dell'unità possibili nel campo.

3. Contributi Chiave

I contributi principali del lavoro sono:

1. Dimostrazione Verificata: Una prova completa e priva di errori (senza assiomi sorry) del teorema di Ramanujan–Nagell.
2. Infrastruttura Riutilizzabile: Sviluppo di librerie per lavorare con gli anelli degli interi dei campi quadratici in Lean 4, inclusa la verifica della fattorizzazione unica e il calcolo del gruppo delle unità. Questa infrastruttura è generalizzabile ad altri campi quadratici.
3. Analisi del Gap Formale: Un'analisi dettagliata delle differenze tra le dimostrazioni sui libri di testo e quelle verificabili da macchina, evidenziando dove le argomentazioni "ovvie" richiedono elaborazioni sostanziali.
4. Uso dell'IA: Il progetto è un caso di studio significativo sull'uso di strumenti di Intelligenza Artificiale (Claude Code e Aristotle) per assistere nella generazione di bozze di prove, nella riparazione di errori causati da aggiornamenti della libreria e nella scoperta di lemmi necessari.

4. Risultati Tecnici e Sfide

La dimostrazione formale conferma che le uniche soluzioni sono:
$$(n, x) \in \{(3, \pm1), (4, \pm3), (5, \pm5), (7, \pm11), (15, \pm181)\}$$

Le sfide tecniche più significative incontrate includono:

• Isomorfismi e Trasporto di Proprietà: La necessità di costruire isomorfismi espliciti tra diverse rappresentazioni dello stesso campo quadratico in Lean e di "trasportare" manualmente le proprietà di chiusura integrale è un compito che nei testi matematici è spesso omesso o trattato come banale.
• Inferenza di Typeclass: Problemi legati ai "diamanti" di typeclass (conflitti tra diverse istanze di strutture algebriche) hanno richiesto l'inserimento manuale di dichiarazioni di istanza (letI, haveI) per evitare ambiguità nel sistema di inferenza di Lean.
• Aritmetica in $O_K$ vs $\mathbb{Z}$: Molte identità algebriche che sono banali sugli interi ($\mathbb{Z}$) richiedono passaggi multipli di coercizione e riscrittura quando eseguite nell'anello degli interi $O_K$, poiché mancano procedure decisionali automatizzate per questo tipo di anelli.
• Espansione Binomiale e Riduzione Modulo 42: La riduzione dell'esponente a tre classi di resto modulo 42 richiede una manipolazione complessa di somme binomiali e reindicizzazioni, gestite tramite combinatoria su Finset.
• Valutazioni $p$-adiche: La parte finale della dimostrazione (unicità della soluzione per classe di resto) si basa su un argomento di valutazione $7$-adica (Lifting the Exponent Lemma), che richiede un'analisi fine delle valuzioni dei coefficienti binomiali.

5. Significato e Impatto

Questo lavoro rappresenta una pietra miliare nella verifica formale della teoria dei numeri:

• È la prima formalizzazione di una congettura di Ramanujan in un assistente di dimostrazione.
• Dimostra la maturità dell'ecosistema Mathlib per gestire problemi avanzati di teoria algebrica dei numeri, inclusi campi quadratici, numeri di classe e gruppi di unità.
• Fornisce un modello per come l'IA generativa può accelerare lo sviluppo di prove formali complesse, riducendo il tempo necessario per la scrittura di codice boilerplate e la ricerca di lemmi, pur mantenendo la verifica formale rigorosa del kernel di Lean.
• Offre un punto di partenza per la formalizzazione di altre equazioni diofantee esponenziali, fornendo un'infrastruttura solida per l'aritmetica nei campi quadratici.

In sintesi, il paper non solo risolve un problema matematico classico in modo verificato, ma espande anche le capacità degli strumenti formali attuali, delineando le sfide e le soluzioni pratiche per la formalizzazione della matematica avanzata.