A formalization of the Gelfond-Schneider theorem

1. Problématique et Contexte

L'article présente la formalisation complète du théorème de Gelfond-Schneider dans l'assistant de preuve Lean 4 (avec la bibliothèque Mathlib). Ce théorème résout la septième question de Hilbert, posée en 1900.

• Énoncé du théorème : Si $\alpha$ et $\beta$ sont des nombres algébriques, avec $\alpha \notin \{0, 1\}$ et $\beta$ irrationnel, alors $\alpha^\beta$ est un nombre transcendant.
• Importance : Ce résultat est une pierre angulaire de la théorie des nombres transcendants, reliant la théorie algébrique des nombres et l'analyse complexe. Il permet d'établir la transcendance de constantes célèbres comme $2^{\sqrt{2}}$, $e^\pi$ (constante de Gelfond) et $i^i$.
• État de l'art : Bien que des preuves de transcendance pour $e$ et $\pi$ (théorème de Lindemann-Weierstrass) aient déjà été formalisées dans divers assistants (HOL Light, Rocq, Isabelle/HOL), aucune preuve du théorème de Gelfond-Schneider n'existait auparavant dans un assistant de preuve.

2. Méthodologie et Architecture de la Preuve

La formalisation suit la preuve constructive originale de Gelfond et Schneider, qui repose sur une méthode auxiliaire (construction d'une fonction auxiliaire) et une contradiction entre une borne inférieure algébrique et une borne supérieure analytique.

A. Fondements Algébriques et Théorie des Nombres

• La "Maison" d'un nombre algébrique (House) : Pour mesurer la taille d'un entier algébrique $\alpha$ dans un corps de nombres $K$, les auteurs définissent la "maison" de $\alpha$ comme le maximum des modules de ses conjugués.
  • Innovation technique : Au lieu d'utiliser une approche naïve basée sur les racines d'un polynôme (qui pose des problèmes de dépendance de types et d'ordonnancement), ils utilisent l'embedding canonique de $K$ dans une algèbre de Banach. Cela permet d'utiliser l'API des espaces normés de Mathlib pour dériver immédiatement les propriétés de norme (inégalité triangulaire, multiplicativité).
• Lemme de Siegel pour les corps de nombres : La preuve nécessite l'existence de coefficients "petits" (entiers algébriques) pour une fonction auxiliaire. Les auteurs formalisent une version généralisée du Lemme de Siegel pour les entiers d'un corps de nombres $O_K$.
  • Stratégie : Ils transforment le système linéaire sur $O_K$ en un système plus grand sur $\mathbb{Z}$ via une représentation de base, résolvent le système sur $\mathbb{Z}$ (déjà présent dans Mathlib), puis relèvent la solution dans $O_K$.

B. Construction de la Fonction Auxiliaire

• Fonction $R(z)$ : Une fonction de la forme $R(z) = \sum \eta_i e^{\rho_i z}$ est construite. Les coefficients $\eta_i$ sont déterminés en imposant que $R(z)$ s'annule avec une multiplicité élevée en des points entiers spécifiques. Cela génère un système d'équations linéaires homogènes sous-déterminé, résolu par le Lemme de Siegel.
• Non-annulation : Il est prouvé que $R(z)$ n'est pas identiquement nulle grâce à l'indépendance linéaire des exponentielles (via une matrice de Vandermonde).

C. Défi Analytique : La Fonction Globale $S(z)$

C'est l'aspect le plus complexe de la formalisation. La preuve classique introduit une fonction $S(z)$ qui est un quotient impliquant $R(z)$ et des pôles aux points entiers.

• Problème des pôles : En analyse classique, on évite les pôles. En théorie des types dépendants, une fonction méromorphe (partielle) compliquerait considérablement la preuve en nécessitant le suivi constant des domaines de définition.
• Solution technique : Les auteurs construisent $S(z)$ comme une fonction totale et holomorphe partout.
  • Ils utilisent une stratégie de "patching" (raccordement) : ils définissent localement des développements en série de Taylor (facteurs locaux) aux points singuliers pour éliminer les pôles, puis raccordent ces définitions locales avec la formule rationnelle valide hors des singularités.
  • Cela permet d'utiliser la formule intégrale de Cauchy sur un contour fermé sans avoir à gérer des types optionnels ou des sous-ensembles pour les domaines de définition.

D. La Contradiction Finale

La preuve se conclut par une estimation contradictoire de la valeur $\rho = (\log \alpha)^{-r} R^{(r)}(l_0)$ :

1. Borne inférieure algébrique : Puisque $\rho$ est un nombre algébrique non nul, sa norme sur $\mathbb{Q}$ est $\ge 1$. Cela implique une borne inférieure sur $|\rho|$ qui décroît exponentiellement avec le paramètre $r$.
2. Borne supérieure analytique : En utilisant la formule intégrale de Cauchy sur un contour englobant les singularités, on obtient une borne supérieure sur $|\rho|$ qui décroît super-exponentiellement (plus vite que la borne inférieure) lorsque $r$ est grand.
3. Conclusion : Pour un $r$ suffisamment grand, l'inégalité devient impossible, prouvant par l'absurde que l'hypothèse de départ ($\alpha^\beta$ algébrique) est fausse.

3. Contributions Clés

• Première formalisation : Il s'agit de la première preuve formelle du théorème de Gelfond-Schneider dans n'importe quel assistant de preuve.
• Gestion explicite des constantes : Contrairement aux preuves papier qui utilisent souvent la notation $O(\cdot)$ ou des constantes génériques, cette formalisation a dû définir et suivre explicitement une séquence de 15 constantes ($c_1$ à $c_{15}$) dépendant du degré du corps de nombres et des propriétés géométriques. Cela a été crucial pour établir la contradiction quantitative finale.
• Analyse complexe formelle avancée : La construction d'une fonction auxiliaire globale holomorphe à partir d'une expression méromorphe classique démontre la maturité des bibliothèques d'analyse complexe de Mathlib (gestion des singularités retirables, raccordement de fonctions).
• Intégration dans Mathlib : Une partie du code développé a déjà été intégrée dans la bibliothèque principale Mathlib, enrichissant les outils disponibles pour la théorie des nombres algébriques et l'analyse.

4. Résultats Concrets

• Théorème principal : La preuve formelle du théorème de Gelfond-Schneider est disponible sous la forme :
  theorem transcendental_cpow_of_isAlgebraic_of_irrational
• Application immédiate : Les auteurs ont utilisé leur cadre formel pour prouver la transcendance de la constante de Gelfond-Schneider spécifique : $\sqrt{2}^{\sqrt{2}}$.

5. Signification et Perspectives

Ce travail marque une étape majeure dans la formalisation des mathématiques profondes :

• Validation de la théorie : Il confirme que les méthodes analytiques complexes (fonctions auxiliaires, estimations de croissance) peuvent être entièrement vérifiées par machine.
• Fondation pour l'avenir : Ce travail ouvre la voie à la formalisation du théorème de Baker (sur les formes linéaires en logarithmes), qui généralise le résultat de Gelfond-Schneider.
• Extensions potentielles :
  • Adaptation aux nombres $p$-adiques (théorème de Gelfond-Schneider $p$-adique).
  • Généralisation aux courbes elliptiques (fonction $\wp$ de Weierstrass).
  • Développement de procédures de décision pour l'indépendance linéaire de logarithmes en utilisant l'arithmétique d'intervalles.
  • Contribution à la vérification conditionnelle de la conjecture de Schanuel.

En résumé, cet article ne se contente pas de vérifier un théorème connu ; il développe une infrastructure robuste pour l'analyse transcendantale formelle, résolvant des défis techniques liés à la gestion des constantes et à la manipulation de fonctions analytiques dans un cadre de types dépendants.