Page web de Benoît Cadorel

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 :