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

Cet article présente une formalisation complète dans Lean 4 du théorème de Ramanujan-Nagell, qui caractérise les solutions entières de l'équation diophantienne $x^2 + 7 = 2^n$, en détaillant la stratégie de preuve, l'architecture du développement et les défis liés à l'infrastructure de la théorie algébrique des nombres requise.

L'essentiel

🧩 Le Grand Puzzle de Ramanujan : Une Enquête Mathématique Vérifiée par un Robot

Imaginez que vous êtes un détective. En 1913, un génie mathématique nommé Ramanujan vous a laissé un mystère sur un bout de papier. Il vous a dit :

"Si vous prenez un nombre, vous le multipliez par lui-même, vous ajoutez 7, et le résultat est une puissance de 2 (comme 2, 4, 8, 16...), alors il n'y a que cinq réponses possibles."

Ces réponses sont des couples de nombres très spécifiques (comme 3 et 1, ou 15 et 181). Ramanujan a dit : "Voici les solutions, et il n'y en a pas d'autres." Un autre mathématicien, Nagell, a prouvé cela en 1948.

Mais dans le monde des mathématiques, une preuve écrite sur du papier peut parfois contenir des "trous" ou des sauts de logique que l'œil humain ne voit pas. C'est là qu'intervient Barinder S. Banwait, l'auteur de ce papier. Il a décidé de construire une preuve infaillible en utilisant un ordinateur spécial appelé Lean 4.

🏗️ L'Analogie : Construire une Cathédrale en Verre

Pour vérifier cette énigme, le chercheur n'a pas seulement écrit la preuve finale. Il a dû construire toute la cathédrale qui la soutient, pierre par pierre, en utilisant un langage que l'ordinateur comprend parfaitement.

Voici comment il a procédé, étape par étape :

1. Le Terrain (Le Monde des Nombres Magiques)
Pour résoudre l'équation, il faut entrer dans un monde spécial appelé $\mathbb{Q}(\sqrt{-7})$.

• L'image : Imaginez que les nombres habituels (1, 2, 3...) sont une route plate et droite. Le monde de Ramanujan est une route qui tourne en spirale dans une dimension invisible (avec des racines carrées de nombres négatifs).
• Le défi : Dans ce monde, les règles sont différentes. Parfois, un nombre qui semble "simple" (comme un entier) se comporte bizarrement. Le chercheur a dû cartographier ce terrain avec une précision chirurgicale pour s'assurer que chaque "brique" (chaque nombre) est bien à sa place.

2. Les Fondations (L'Infrastructure)
Avant de prouver le théorème, il a dû prouver que les fondations de ce monde sont solides.

• L'unicité de la construction : Il a dû prouver que dans ce monde spécial, on ne peut pas décomposer un nombre de deux façons différentes (comme si un Lego pouvait être démonté en deux ensembles de pièces totalement différents). C'est ce qu'on appelle la "factorisation unique".
• Les gardiens (Les Unités) : Il a dû identifier les "gardes du corps" de ce monde (les nombres qui, multipliés par n'importe quoi, ne changent rien). Il a prouvé qu'il n'y avait que deux gardes : +1 et -1.

3. Le Pont entre deux Mondes
C'est ici que ça devient technique. Le monde mathématique peut être décrit de deux façons différentes (comme décrire une maison soit par ses fenêtres, soit par ses portes).

• Le problème : L'ordinateur ne voit pas que ces deux descriptions sont la même maison. Pour lui, ce sont deux bâtiments différents.
• La solution : Le chercheur a dû construire un pont (une isomorphie) pour dire à l'ordinateur : "Hé, regarde, si tu traverses ce pont, la maison A devient exactement la maison B". Sans ce pont, l'ordinateur serait resté bloqué.

4. L'Enquête Finale (La Preuve)
Une fois le terrain sécurisé, il a appliqué la logique de Ramanujan :

• Il a divisé le problème en deux cas : quand le nombre est pair et quand il est impair.
• Pour le cas impair, il a utilisé une expansion binomiale (une sorte de recette de cuisine mathématique qui mélange des termes).
• Il a ensuite appliqué un filtre magique (la division par 7) qui a éliminé 99% des possibilités, ne laissant que trois pistes suspectes.
• Enfin, il a prouvé que dans chacune de ces trois pistes, il n'y a qu'une seule solution possible.

🤖 Le Rôle de l'Intelligence Artificielle (Le Co-pilote)

Ce qui rend ce papier très moderne, c'est l'utilisation de l'IA (comme Claude Code et Aristotle).

• L'analogie : Imaginez que vous écrivez un roman. Vous savez l'histoire, mais l'orthographe et la grammaire sont complexes. L'IA est comme un assistant qui vous dit : "Pour cette phrase, le mot 'pomme' ne va pas, essaye 'poire', et voici la phrase suivante toute faite."
• L'IA n'a pas inventé la preuve. Elle a aidé à écrire les phrases techniques, à trouver les bons mots dans le dictionnaire géant de l'ordinateur (Mathlib), et à corriger les erreurs de frappe. Mais c'est l'humain qui a gardé le contrôle du scénario.

🏆 Pourquoi est-ce important ?

Ce travail est une première mondiale :

1. C'est la première fois qu'une conjecture de Ramanujan est entièrement vérifiée par un ordinateur.
2. C'est la première fois qu'une équation aussi complexe est résolue de bout en bout dans un système de vérification formelle.

En résumé, ce papier ne nous apprend pas une nouvelle réponse mathématique (nous savions déjà quelles étaient les solutions). Il nous apprend comment nous pouvons désormais faire confiance à ces réponses à 100 %, car un robot a vérifié chaque virgule, chaque hypothèse et chaque logique, sans jamais se tromper, sans jamais être fatigué, et sans jamais faire de "saut de logique".

C'est comme passer d'une carte dessinée à la main à un GPS satellite ultra-précis pour naviguer dans l'univers des nombres.

Résumé technique

1. Problème et Contexte

L'article présente la formalisation complète et vérifiée par machine du théorème de Ramanujan-Nagell dans le prouveur de théorèmes interactif Lean 4, en utilisant la bibliothèque standard Mathlib.

Le problème central est la résolution de l'équation diophantienne exponentielle suivante :
$$x^2 + 7 = 2^n$$
où $x$ et $n$ sont des entiers. Ramanujan a conjecturé en 1913 que les seules solutions entières pour $n$ sont $3, 4, 5, 7, 15$. Nagell a prouvé cette conjecture en 1948. L'ensemble complet des solutions $(n, x)$ est :
$$\{(3, \pm1), (4, \pm3), (5, \pm5), (7, \pm11), (15, \pm181)\}$$

C'est la première formalisation d'une conjecture de Ramanujan dans un assistant de preuve, et la première résolution complète d'une équation diophantienne exponentielle spécifique dans un système de vérification formelle.

2. Méthodologie et Architecture

La preuve formelle suit la démonstration classique (exposée par Stewart et Tall) qui utilise la théorie algébrique des nombres, mais l'adapte rigoureusement aux contraintes de Lean 4.

Structure du Code

La formalisation est répartie sur cinq fichiers (environ 3 570 lignes de code et 125 déclarations) :

1. QuadraticIntegerROI.lean & RingOfIntegers.lean : Identification de l'anneau des entiers $\mathcal{O}_K$ du corps quadratique $K = \mathbb{Q}(\sqrt{-7})$.
2. FieldIsomorphism.lean : Établissement d'un isomorphisme entre deux présentations du même corps (l'une générée par $\sqrt{-7}$, l'autre par $\frac{1+\sqrt{-7}}{2}$).
3. Helpers.lean : Calcul des invariants algébriques (discriminant, nombre de classes, groupe des unités) et preuve de l'irréductibilité des éléments clés.
4. Basic.lean : La preuve principale, incluant la factorisation unique, la réduction modulo 42 et l'unicité des solutions par classe de congruence.

Stratégie de Preuve

La preuve se déroule en plusieurs étapes logiques :

• Cas pair : Si $n$ est pair, une factorisation directe dans $\mathbb{Z}$ donne la solution unique $n=4$.
• Cas impair : Si $n$ est impair, l'équation est réécrite dans l'anneau des entiers $\mathcal{O}_K = \mathbb{Z}[\theta]$ où $\theta = \frac{1+\sqrt{-7}}{2}$.
• Factorisation unique : L'équation devient $(\frac{x+\sqrt{-7}}{2})(\frac{x-\sqrt{-7}}{2}) = \theta^m \theta'^m$. Grâce à l'unicité de la factorisation (car $\mathcal{O}_K$ est un anneau principal), on déduit que $\frac{x+\sqrt{-7}}{2} = \pm \theta^m$ (ou son conjugué).
• Réduction modulo 7 : En développant par le théorème binomial et en réduisant modulo 7, on montre que $m$ doit appartenir à l'une des trois classes de congruence modulo 42 : $m \equiv 3, 5, 13 \pmod{42}$.
• Unicité : On prouve par contradiction (en utilisant des valuations $p$-adiques, spécifiquement la valuation 7-adique) qu'au plus une solution existe par classe de congruence.

3. Contributions Clés et Résultats Techniques

Infrastructure Algébrique

L'auteur a dû construire une infrastructure robuste pour travailler avec les anneaux d'entiers quadratiques dans Lean :

• Identification de $\mathcal{O}_K$ : Preuve formelle que pour $d \equiv 1 \pmod 4$, l'anneau des entiers de $\mathbb{Q}(\sqrt{d})$ est $\mathbb{Z}[\frac{1+\sqrt{d}}{2}]$.
• Propriétés de $\mathcal{O}_K$ :
  • Calcul du discriminant : $-7$.
  • Preuve que le nombre de classes est 1 (donc $\mathcal{O}_K$ est un anneau principal, PID, et donc un domaine à factorisation unique, UFD).
  • Détermination du groupe des unités : $\mathcal{O}_K^\times = \{\pm 1\}$.
• Isomorphisme de corps : Gestion explicite de l'isomorphisme entre la présentation standard de Mathlib ($\omega^2 = -7$) et la présentation nécessaire pour les entiers ($\omega^2 = -2 + \omega$).

Résultats de Preuve

• Preuve machine vérifiée : Le théorème principal est prouvé sans aucune hypothèse non vérifiée (sorry). Il ne dépend que des axiomes standards de Lean.
• Généralisation : L'infrastructure développée pour $\mathbb{Q}(\sqrt{-7})$ est conçue pour être généralisable à d'autres corps quadratiques.

4. Défis Rencontrés et Différences avec la Preuve "Papier"

L'article met en lumière l'écart significatif entre les preuves mathématiques informelles et leur formalisation :

• Transfert entre présentations de corps : En mathématiques, on considère souvent $\mathbb{Q}(\sqrt{-7})$ comme un objet unique. En Lean, les types définis par différents générateurs sont distincts. L'auteur a dû construire un isomorphisme explicite d'algèbres sur $\mathbb{Q}$ et transporter manuellement les propriétés d'intégralité (clôture intégrale).
• Inférence de classes de type (Typeclass Inference) : Des problèmes de "diamants" (diamonds) sont apparus lorsque plusieurs instances d'algèbres étaient disponibles pour le même type. L'auteur a dû utiliser des injections manuelles (letI, haveI) pour résoudre les ambiguïtés.
• Arithmétique dans $\mathcal{O}_K$ vs $\mathbb{Z}$ : Des identités triviales dans $\mathbb{Z}$ (comme $\theta^2 = \theta - 2$) nécessitent des coercions explicites vers le corps des fractions $K$ et des réécritures complexes dans $\mathcal{O}_K$, car les tactiques d'arithmétique linéaire (linarith) ne fonctionnent pas directement sur les entiers algébriques.
• Détermination du groupe des unités : La preuve que les seules unités sont $\pm 1$ est laborieuse. Elle nécessite d'exclure les racines de l'unité d'ordre 3, 4 et 6 en résolvant des systèmes d'équations diophantiennes via la tactique omega, ce qui est très coûteux en temps de calcul.
• Développement binomial et réindexation : La preuve de la réduction modulo 42 nécessite une manipulation fine des sommes finies (Finset), y compris des réindexations complexes (sum_bij) qui sont souvent omises dans les manuels.

5. Rôle de l'IA et Perspectives

Un aspect notable de ce projet est l'utilisation intensive d'outils d'IA générative (Claude Code et Aristotle) pour :

• Suggérer des tactiques et des séquences de preuves.
• Réparer les preuves lors des mises à jour de la bibliothèque Mathlib.
• Découvrir des lemmes pertinents dans la vaste API de Mathlib.
• Générer du code répétitif (boilerplate) pour les cas de figure multiples.

L'auteur conclut que l'IA a considérablement réduit la barrière d'entrée pour la formalisation, bien que la vérification finale reste strictement du ressort du noyau de Lean.

6. Signification

Ce travail démontre la maturité actuelle de l'écosystème Mathlib pour traiter des sujets avancés de théorie algébrique des nombres. Il valide non seulement un résultat historique célèbre, mais fournit également une infrastructure réutilisable pour les anneaux d'entiers quadratiques. Cela ouvre la voie à la formalisation de problèmes diophantiens plus complexes et à l'intégration de l'IA comme partenaire standard dans le processus de preuve formelle.