Second semestre 2024-2025
Preuves assistées par ordinateur. L1 Mathématiques.
Je donne un cours de preuves assistées par ordinateur, reposant sur l'assistant de preuve LEAN. L'objectif de ce cours -- principalement composé de séances de TP -- est de permettre aux étudiant·es de travailler l'écriture de preuves mathématiques, en se servant de la machine comme guide.
Les documents de cours sont tous disponibles ici :
- Diaporama du cours et compléments :
- Séances de TP :
- Documents essentiels :