teorth/analysis : un compagnon Lean pour Analysis I
Un compagnon Lean de l'Analyse I. Par exemple, le chapitre 2 développe une théorie des nombres naturels indépendante de Mathlib, mais tous les chapitres suivants utiliseront à la place les nombres naturels Mathlib.
En bref
- De quoi s’agit-il ?
- Une formalisation Lean fidèle d'Analysis I de Terence Tao, avec une transition progressive vers les définitions de Mathlib et quelques contenus Lean annexes sans rapport avec le manuel.
- À qui s’adresse-t-il ?
- Le README présente le dépôt comme un compagnon annoté d'Analysis I plutôt qu'un remplacement, et la liste des chapitres le confirme : chapitres 2 à 11 plus annexes A et B, le chapitre 1 étant délibérément absent. Le dépôt héberge aussi des travaux Lean sans rapport avec le manuel, notamment la théorie de la mesure, des systèmes d'unités et plusieurs entrées liées à des problèmes d'Erdős, le tout sous la même licence Apache-2.0.
- Puis-je l’utiliser commercialement ?
- Oui. Apache-2.0 est une licence permissive : vous pouvez utiliser, modifier et vendre un logiciel qui en dépend, à condition de conserver les mentions de droit d’auteur et de licence.
- Est-il encore maintenu ?
- Oui. Les derniers commits datent d’il y a 11 jours.
- En quel langage est-il écrit ?
- Principalement Lean, d’après les statistiques de langage de GitHub.
Ces réponses reposent sur les données GitHub du projet (dernière synchronisation le 14 septembre 2026) et sur notre analyse. Elles ne constituent pas un avis juridique.
ANALYSE OPEN SOURCE APPROFONDIE
Un compagnon Lean pour Analysis I
Ce dépôt contient une formalisation du livre Analysis I de Terence Tao écrite avec l'assistant de preuve Lean. Le README la présente comme une paraphrase aussi fidèle que possible du manuel, visant à rester proche du texte original tout en montrant les fonctionnalités et la syntaxe de Lean. L'auteur précise que la formalisation n'est pas optimisée pour l'efficacité et peut parfois s'écarter de l'usage idiomatique de Lean. Les passages laissés en exercice au lecteur dans le livre apparaissent dans cette traduction sous forme de sorry. L'auteur n'a pas l'intention de placer les solutions directement dans le dépôt et invite les lecteurs à forker le projet pour tenter ces exercices. Le README indique aussi que la formalisation ne cite pas directement le manuel, mais renvoie au texte original aux endroits appropriés, de sorte qu'elle doit être considérée comme un compagnon annoté du manuel plutôt que comme un remplacement.
La transition progressive vers les définitions de Mathlib
Une grande partie du contenu d'Analysis I existe déjà dans Mathlib, la bibliothèque mathématique standard de Lean, mais avec des définitions légèrement différentes. Le README explique comment la formalisation concilie ces différences : elle passe progressivement des définitions du manuel à celles de Mathlib au fur et à mesure que l'on avance dans le texte. Le chapitre 2 développe par exemple une théorie des entiers naturels indépendante de Mathlib, mais tous les chapitres suivants utilisent les entiers naturels de Mathlib. Un épilogue au chapitre 2 montre que les deux notions sont isomorphes. Le même schéma apparaît pour les réels : un épilogue du chapitre 5 prouve un isomorphisme avec les réels de Mathlib, et le chapitre 6 comporte un épilogue reliant ses limites à celles de Mathlib. Grâce à cette conception, le README suggère que la formalisation peut aussi servir d'introduction à diverses parties de Mathlib.
Changements techniques par rapport au manuel
Un petit nombre de définitions diffèrent du livre pour que la formalisation s'aligne sur les conventions de Mathlib. Le README en signale trois. Les suites sont indexées à partir de zéro plutôt que de un, car Mathlib offre beaucoup plus de support pour les entiers naturels basés sur zéro. Les opérations laissées non définies dans le manuel, comme la division par zéro ou la prise de limite formelle d'une suite non de Cauchy, reçoivent une valeur de rechange (par exemple 0), ce qui rend chaque opération totale. Le README explique ce choix en notant que Lean gère mieux les fonctions totales que les fonctions partielles, et renvoie à un article de blog de Kevin Buzzard sur la division par zéro en théorie des types. Enfin, les entiers naturels du chapitre 2 sont construits comme un type inductif plutôt que par une approche purement axiomatique, les axiomes de Peano étant formalisés dans l'épilogue du chapitre.
Couverture et organisation
Le chapitre 1 du livre n'est pas formalisé. Tout ce qui va du chapitre 2 au chapitre 11 est présent, ainsi que l'annexe A sur les bases de la logique mathématique et l'annexe B sur le système décimal. L'ordre des chapitres va des entiers naturels, de la théorie des ensembles, des entiers et des rationnels, et des nombres réels, aux limites de suites, aux séries, aux ensembles infinis, aux fonctions continues, à la différentiation et à l'intégrale de Riemann. Pour chaque section, le README fournit trois liens : une page Verso rendant le contenu formalisé, une documentation HTML générée et le fichier source Lean. Les noms de sections suivent la structure du livre, de la section 2.1 sur les axiomes de Peano à la section 11.10 sur les conséquences du théorème fondamental du calcul, de sorte que la navigation dans le dépôt suit l'ordre du manuel.
Autres contenus Lean du dépôt
Au-delà de la formalisation d'Analysis I, le dépôt héberge plusieurs projets Lean sans rapport avec le manuel, sous une rubrique intitulée Additional content. Le README indique que l'auteur utilise ce dépôt pour héberger d'autres contenus Lean mineurs non liés au livre. Une formalisation du livre de l'auteur sur la théorie de la mesure est présente et marquée comme travail en cours. Il y a un support pour les systèmes d'unités physiques, y compris le système SI, chacun avec des exemples d'utilisation. Le dépôt contient aussi une formalisation du choix fini qui évite l'axiome du choix de Lean, une théorie des probabilités finie et quatre entrées liées à des problèmes d'Erdős : une solution au numéro 379, le contre-exemple de Pikhurko au numéro 613, et des solutions aux numéros 707 et 987. Chacune de ces extensions a ses propres liens de documentation et de source dans le README. Seule la formalisation de la théorie de la mesure est explicitement marquée comme inachevée.
Construction du projet et de la page web
Le README documente deux chemins de construction. Après avoir installé Lean et cloné le dépôt, exécuter ./build.sh construit le projet lui-même. Exécuter ./build-web.sh construit la page web du projet, la sortie étant placée dans _site/, qui peut ensuite être servie avec python3 serve.py. La mise à jour des versions de Lean et de Mathlib est un processus manuel : il faut modifier lakefile.lean pour changer les lignes require de Mathlib et doc-gen4, changer le fichier lean-toolchain, puis exécuter lake update -R -Kenv=dev. Le README avertit que cette opération peut définir la toolchain sur la dernière version de Lean, auquel cas il faut la rétablir, et note que le projet utilise une méthode obsolète pour exiger doc-gen4 conditionnellement.
Licence et ressources externes
Le dépôt est distribué sous licence Apache 2.0. L'extrait de licence accorde une licence de droit d'auteur perpétuelle, mondiale, non exclusive, gratuite, sans redevance et irrévocable pour reproduire, préparer des œuvres dérivées, afficher publiquement, exécuter publiquement, sous-licencier et distribuer l'œuvre. Il accorde également une licence de brevet couvrant les revendications nécessairement enfreintes par les contributions d'un contributeur, la licence prenant fin si le destinataire engage une action en contrefaçon de brevet. L'extrait ne dit rien sur la garantie, le support ou la sécurité, et le README ne fait aucune déclaration à ces sujets. Le README renvoie aussi à la page web du projet, à la page web du livre et à son édition Springer, à un article de blog annonçant le projet, à un canal de discussion Lean Zulip, à des notes pour les contributeurs et à une formalisation Lean distincte d'Analysis II créée par une autre équipe.
Conclusion éditoriale
Le README présente le dépôt comme un compagnon annoté d'Analysis I plutôt qu'un remplacement, et la liste des chapitres le confirme : chapitres 2 à 11 plus annexes A et B, le chapitre 1 étant délibérément absent. Le dépôt héberge aussi des travaux Lean sans rapport avec le manuel, notamment la théorie de la mesure, des systèmes d'unités et plusieurs entrées liées à des problèmes d'Erdős, le tout sous la même licence Apache-2.0.
Notes de la communauté