Formalisation de l'Analyse I dans Lean : un projet d'apprentissage interactif

L'auteur formalise son manuel d'analyse réelle vieux de 20 ans, « Analyse I », à l'aide de l'assistant de preuve Lean. Il ne s'agit pas d'une simple traduction ; cela implique de convertir les définitions, les théorèmes et les exercices en code Lean. Les lecteurs peuvent effectuer les exercices en remplissant les « sorries » dans le code, en apprenant Lean et la bibliothèque Mathlib au fur et à mesure. Le projet comprend actuellement plusieurs sections traduites, effectuant une transition stratégique de la construction « manuelle » des nombres naturels à la bibliothèque standard Mathlib. L'auteur invite les bénévoles à tester et à améliorer le projet.