Un compagnon Lean pour "Analyse I" : Quand les mathématiques rigoureuses rencontrent la vérification formelle
Il y a près de 20 ans, j'ai publié un manuel d'analyse réelle intitulé "Analyse I". Ce livre se distinguait en abordant les fondements des mathématiques, comme la construction des nombres naturels, entiers, rationnels et réels, tout en intégrant des éléments de théorie des ensembles et de logique. Aujourd'hui, je lance un projet complémentaire utilisant Lean, un assistant de preuve, pour formaliser les concepts du manuel.
À l'époque de la rédaction, les assistants de preuve comme Coq ou Agda existaient déjà, mais la vérification formelle n'était pas dans mon champ de vision. Mon expérience récente avec Lean m'a fait réaliser que le contenu de "Analyse I" s'y prête parfaitement. La "théorie des types naïve" implicite dans le livre correspond bien à la théorie des types dépendants de Lean.
Ce compagnon Lean propose une traduction des définitions, théorèmes et exercices du manuel en code Lean. Les exercices peuvent ainsi être résolus en complétant les "sorries" (espaces à remplir) dans le code. Je n'ai pas prévu de fournir de solutions officielles, mais les utilisateurs peuvent créer des forks du dépôt pour partager leurs réponses.
Actuellement, plusieurs sections ont été traduites : les nombres naturels, l'addition, la multiplication, la théorie des ensembles de base et les entiers. La formalisation alterne entre des développements indépendants et l'utilisation de la bibliothèque standard Mathlib de Lean.
Par exemple, pour les nombres naturels, j'ai d'abord construit manuellement une version alternative (Chapter2.Nat), avec des résultats de base établis comme exercices. Ensuite, une section épilogue établit des isomorphismes avec les nombres naturels de Mathlib, après quoi cette version alternative est abandonnée.
Cette approche progressive permet de s'appuyer de plus en plus sur Mathlib dans les chapitres avancés. Ainsi, ce projet sert à la fois d'introduction à l'analyse réelle et à Lean/Mathlib, dans l'esprit du "Natural number game" qui recoupe largement le chapitre 2 de mon manuel.
Le code du dépôt compile dans Lean, mais je n'ai pas vérifié si tous les "sorries" peuvent être résolus. J'invite des volontaires à tester le compagnon et à fournir des retours sur la faisabilité des exercices et l'adéquation des lemmes d'aide fournis.
[Mise à jour du 31 mai : le compagnon a été déplacé vers un dépôt indépendant.]
