A formalization of the Gelfond-Schneider theorem

1. Il Problema e il Contesto

Il lavoro si concentra sulla formalizzazione in Lean 4 (utilizzando la libreria Mathlib) del Teorema di Gelfond-Schneider, che risolve il settimo problema di Hilbert.

• Enunciato del Teorema: Se $\alpha$ e $\beta$ sono numeri algebrici, con $\alpha \neq 0, 1$ e $\beta$ irrazionale, allora il numero $\alpha^\beta$ è trascendente.
• Importanza: Questo risultato è una pietra miliare della teoria dei numeri trascendenti, collegando la teoria dei numeri algebrici e l'analisi complessa. Prima di questa formalizzazione, non esisteva alcuna prova assistita da computer di questo teorema profondo, sebbene fossero stati formalizzati risultati più semplici (come la trascendenza di $e$ e $\pi$ o di numeri di Liouville).
• Esempio chiave: Il teorema garantisce la trascendenza di costanti come $2^{\sqrt{2}}$ (la costante di Gelfond-Schneider) e $e^\pi$.

2. Metodologia e Architettura della Formalizzazione

Gli autori hanno dovuto tradurre una dimostrazione classica, che fa ampio uso di argomentazioni analitiche e stime asintotiche, in un sistema di logica formale rigoroso. La metodologia si divide in due fasi principali: costruzione algebrica e analisi complessa.

A. Fondamenti di Teoria dei Numeri Algebrici

Per gestire le proprietà dei coefficienti dell'funzione ausiliaria, gli autori hanno implementato:

• La "Casa" di un numero algebrico (House): Invece di usare la definizione classica basata sul massimo modulo delle radici del polinomio minimo (che crea problemi di dipendenza dai tipi e ordinamento), hanno definito la "casa" di un numero algebrico $\alpha$ come la norma $L_\infty$ dell'immagine di $\alpha$ tramite l'immersione canonica nello spazio delle funzioni continue sui coniugati. Questo approccio, basato su spazi normati, ha semplificato notevolmente le dimostrazioni delle disuguaglianze triangolari e moltiplicative.
• Lemma di Siegel per Campi di Numeri: La dimostrazione richiede l'esistenza di soluzioni intere "piccole" per sistemi lineari sottodeterminati. Gli autori hanno generalizzato il Lemma di Siegel classico (valido per $\mathbb{Z}$) agli interi algebrici di un campo di numeri $K$. Hanno utilizzato un argomento di discesa: trasformare il sistema su $OK$ in un sistema più grande su $\mathbb{Z}$, applicare il lemma classico e poi "sollevare" la soluzione in $OK$.

B. Costruzione Analitica e Funzioni Ausiliarie

Il cuore della dimostrazione è la costruzione di una funzione ausiliaria $R(z)$ e di una funzione globale $S(z)$:

1. Funzione Ausiliaria $R(z)$: Definita come una combinazione lineare di esponenziali $R(x) = \sum \eta_i e^{\rho_i x}$, dove i coefficienti $\eta_i$ sono interi algebrici ottenuti tramite il Lemma di Siegel. La funzione è costruita per annullarsi con alta molteplicità in punti specifici.
2. Gestione delle Singolarità (Sfida Tecnica Principale): Nella prova classica, si introduce una funzione $S(z)$ che ha poli removibili in punti interi. In Lean, una definizione meromorfa parziale è problematica. Gli autori hanno risolto questo problema costruendo $S(z)$ come una funzione totale e analitica ovunque (piecewise holomorphic).
   • Hanno definito localmente la funzione nei punti singolari usando lo sviluppo in serie di potenze (rimuovendo il polo).
   • Hanno "incollato" (gluing) queste definizioni locali con la formula razionale valida fuori dai punti singolari.
   • Hanno dimostrato formalmente che la funzione risultante è analitica su tutto il piano complesso, utilizzando le librerie di analisi complessa di Mathlib.

C. La Strategia della Contraddizione

La dimostrazione procede per assurdo, confrontando due limiti per una quantità $\rho$ derivata dalle derivate di $R(z)$:

• Limite Algebrico (Inferiore): Poiché $\rho$ è un numero algebrico non nullo, il suo prodotto per i suoi coniugati (la norma) è almeno 1. Questo fornisce un limite inferiore esponenziale che decresce lentamente.
• Limite Analitico (Superiore): Utilizzando la formula integrale di Cauchy su un cerchio che racchiude i punti singolari, si dimostra che $|\rho|$ può essere reso arbitrariamente piccolo scegliendo parametri sufficientemente grandi.
• Contraddizione: Per $r$ (l'ordine di annullamento) sufficientemente grande, il limite analitico diventa più piccolo del limite algebrico, generando una contraddizione.

3. Contributi Chiave e Dettagli Implementativi

• Prima Formalizzazione: Questo è il primo formalizzazione del Teorema di Gelfond-Schneider in qualsiasi assistente di prova.
• Gestione Esplicita delle Costanti: A differenza delle prove classiche che usano la notazione $O(\cdot)$ o costanti generiche, gli autori hanno dovuto tracciare esplicitamente una sequenza di 15 costanti ($c_1, \dots, c_{15}$) dipendenti dal grado del campo e dalle proprietà geometriche. Questo è stato cruciale per stabilire la contraddizione finale.
• Architettura dei Dati: L'uso dell'immersione canonica per definire la "casa" di un numero ha permesso di evitare la gestione manuale dei tipi dipendenti e delle prove di non-vuoto, sfruttando l'infrastruttura degli spazi normati di Mathlib.
• Integrazione in Mathlib: Parti del codice sviluppato sono già state integrate nella libreria principale di Mathlib, arricchendo la teoria dei numeri algebrici e l'analisi complessa.

4. Risultati

• Dimostrazione Completa: Gli autori hanno dimostrato formalmente il teorema: Transcendental Q (α ^ β).
• Verifica di Esempi: Come controllo di correttezza, hanno dimostrato la trascendenza della costante specifica $\sqrt{2}^{\sqrt{2}}$.
• Codice Aperto: Il codice sorgente è disponibile pubblicamente su un ramo di Mathlib.

5. Significato e Prospettive Future

• Avanzamento della Matematica Formale: Questo lavoro dimostra che è possibile formalizzare teoremi profondi che richiedono tecniche analitiche sofisticate (non solo algebra pura), colmando un divario significativo nella teoria dei numeri trascendenti formalizzata.
• Fondazione per Estensioni:
  • Teorema di Baker: La struttura algebrica della prova è indipendente dall'immersione complessa, aprendo la strada alla formalizzazione del teorema di Baker sulle forme lineari nei logaritmi.
  • Teorema p-adico: Sostituendo l'analisi complessa con l'analisi p-adica (integrali di Schnirelmann), si potrebbe formalizzare il teorema di Gelfond-Schneider p-adico.
  • Curve Ellittiche: Il framework potrebbe essere esteso alle curve ellittiche, utilizzando la funzione $\wp$ di Weierstrass al posto dell'esponenziale.
  • Teorema di Schneider-Lang: Le tecniche di funzioni ausiliarie sono centrali anche per questo teorema più generale.
• Decision Procedures: La natura esplicita delle costanti calcolate suggerisce la possibilità di sviluppare procedure decisionali automatizzate per verificare l'indipendenza algebrica di specifici insiemi di logaritmi.

In sintesi, questo lavoro rappresenta un passo fondamentale verso la verifica computerizzata di risultati profondi della matematica moderna, trasformando una dimostrazione analitica classica in un oggetto formale rigoroso e verificabile.