Lean4 et Mathlib

Installation et démarrage

Vous pouvez consulter la documentation officielle.

Pour ma part, j’utilise le système d’exploitation Debian. Cette distribution GNU/Linux fournit le paquet elan qui fournit les outils pour installer Lean et gérer les projets.

Il faut ensuite un éditeur de texte adapté.

• VS-Code de Microsoft (ou sa version plus libre vscodium fournit un plugin special pour Lean (qui doit aussi installer lean).
• J’utilise neovim avec le plugin lean.vim.

Références pour commencer

• le blog First steps in Lean pour le démarrage
• le livre de Mathematics in Lean de Jeremy Avigad et Patrick Massot
• le survol des tactiques pour savoir quels mots-clés utiliser pour manipuler hypothèses ou objectifs.

Module LU3MA263

Pour apprendre à utiliser cet outil, j’écris des preuves formelles pour certains exercices du module de théorie de la mesure.

https://plmlab.math.cnrs.fr/boutilli/lu3ma263-lean.git