Contexte et portée
Le dépôt fermats-last-theorem propose une preuve entièrement vérifiée du dernier théorème de Fermat dans Lean 4, version 4.33.1, en s’appuyant sur Mathlib v4.33.0. La démonstration reproduit le raisonnement de Frey, Serre, Ribet, Wiles et Taylor‑Wiles, mais chaque étape est traduite en un théorème Lean identifié dans PROOF-PATH.md. Le résultat final est le théorème fermats_last_theorem qui affirme que pour tout entier naturel n ≥ 3 et tout a, b, c > 0, l’égalité a^n + b^n = c^n est impossible.
Architecture du dépôt et processus de construction
Le projet comporte 60 475 modules Lean. La compilation s’effectue avec lake, qui télécharge et compile Mathlib depuis les sources — une opération d’environ 13 minutes avec 96 threads. Chaque thread consomme ~5 GB de RAM, ce qui porte le pic de mémoire à 153 GB pendant la construction, qui dure 5 h 32 min. Le répertoire .lake/ occupe 67 GB, tandis que les fichiers C générés atteignent 220 GB, supprimables après la compilation.
Vérification formelle et audit des axiomes
Le cœur de la vérification repose sur trois axiomes du noyau Lean : propext, Classical.choice et Quot.sound. Le fichier FinalCheck.lean confirme cette contrainte :
#guard_msgs in
#print axioms fermat_last_theorem
Le script comparator (version v4.33.0) a re‑joué 1 052 234 déclarations sans erreur, confirmant l’absence d’axiomes additionnels. Un deuxième noyau, nanoda 0.4.13, a importé l’environnement exporté et a vérifié les mêmes déclarations, nécessitant 300 GB de mémoire et 15 heures de temps CPU, dont 30 minutes pour la phase de vérification multithreadée. Aucun module ne contient de sorry, native_decide, unsafe ou d’autres constructions non‑déterministes.
Navigation et exploitation du résultat
Le répertoire html/ (≈ 390 MB) génère une interface web statique consultable hors‑ligne. Il expose 29 511 pages de théorèmes, chacune affichant la déclaration Lean, ses citations et un graphe de dépendances extensible, ainsi que 1 450 pages de modules de définition. Un champ de recherche permet de filtrer les noms, et les graphes de théorèmes majeurs offrent une vue d’ensemble de la structure logique du développement.
Limites et perspectives
La preuve repose entièrement sur la confiance accordée au noyau Lean (ou à nanoda) et aux outils de construction. Aucun mécanisme automatisé ne valide la correspondance sémantique entre les noms de théorèmes et leurs contenus mathématiques ; cette vérification reste du ressort du lecteur. Le projet ne supporte pas Windows, nécessite Linux ou macOS, et n’accepte plus de contributions. Malgré ces contraintes, le dépôt constitue une référence concrète de formalisation complète d’un résultat mathématique de premier plan dans un environnement de preuve assistée par ordinateur.
