Formation Lean : Assistant de preuve

Programme de notre formation Lean

[Jour 1 – Matin]

Prendre en main Lean 4 et le workflow de preuve

• Installer Lean 4 et configurer l’environnement avec VS Code et Lake
• Comprendre le rôle de Lean comme langage fonctionnel et assistant de preuve
• Manipuler les notions fondamentales : Prop, Type, variables, termes et propositions
• Comprendre la boucle de preuve : objectifs, hypothèses, tactiques et messages d’erreur
• Écrire des preuves simples avec by, intro, exact et apply
• Atelier pratique : configurer un projet Lean 4 et formaliser plusieurs implications élémentaires.

[Jour 1 – Après-midi]

Construire et automatiser des preuves en logique propositionnelle

• Manipuler implications, conjonctions et disjonctions avec constructor, cases, left et right
• Raisonner avec la négation et la contradiction grâce à by_contra, contradiction et exfalso
• Manipuler l’égalité avec rfl et effectuer des réécritures avec rw
• Structurer les démonstrations avec have, les sous-preuves et les lemmes intermédiaires
• Utiliser simp, simp? et aesop pour automatiser les preuves tout en comprenant leurs limites
• Atelier pratique : formaliser plusieurs propriétés de logique propositionnelle puis simplifier et fiabiliser leurs preuves.

[Jour 2 – Matin]

Manipuler les quantificateurs, fonctions et théorèmes de Mathlib

• Formaliser des propositions utilisant les quantificateurs ∀ et ∃
• Construire et extraire des preuves existentielles avec les tactiques adaptées
• Raisonner sur les fonctions et utiliser l’extensionalité avec funext
• Formaliser des propriétés simples sur les nombres naturels et autres types fondamentaux
• Rechercher et réutiliser les définitions et théorèmes disponibles dans Mathlib
• Atelier pratique : formaliser des énoncés quantifiés et construire leurs preuves en réutilisant les résultats disponibles dans Mathlib.

[Jour 2 – Après-midi]

Maîtriser l’induction et construire des preuves robustes

• Comprendre le principe de l’induction et construire une preuve par induction sur Nat
• Définir des fonctions récursives et démontrer leurs propriétés
• Structurer les calculs et transformations successives avec calc
• Utiliser les tactiques de simplification et de normalisation adaptées au problème
• Diagnostiquer les preuves incomplètes ou fragiles à partir des objectifs et messages de Lean
• Atelier pratique : démontrer plusieurs propriétés par induction puis refactorer les preuves afin d’améliorer leur lisibilité et leur robustesse.

[Jour 3 – Matin]

Travailler avec les types inductifs, structures et listes

• Définir et manipuler des types inductifs, leurs constructeurs et leurs différents cas
• Raisonner par cas et par induction sur des structures de données
• Manipuler les listes et leurs opérations fondamentales avec List
• Définir des structures, champs et projections et raisonner sur leurs propriétés
• Construire des lemmes réutilisables et les intégrer aux mécanismes de simplification
• Atelier pratique : définir une fonction sur des listes et démontrer plusieurs propriétés concernant son comportement.

[Jour 3 – Après-midi]

Mini-projet de vérification formelle avec Lean

• Transformer une propriété informelle en spécification formelle exploitable par Lean
• Décomposer le problème en définitions, propositions et lemmes intermédiaires
• Organiser les fichiers, namespaces, sections et dépendances du projet
• Choisir entre preuve explicite, réécriture, simplification et automatisation selon le contexte
• Refactorer et documenter les preuves pour améliorer leur lisibilité, robustesse et maintenabilité
• Atelier pratique : réaliser un mini-projet complet, de la spécification formelle à la preuve finale vérifiée par Lean.