Second semestre 2025-2026

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 actuels sont disponibles ici :

• Diaporama du cours et compléments :

• Diaporama de la première séance

• 1. Types et fonctions - Compléments sur le TP 1

• 2. Définir des fonctions - Compléments et quelques exercices

• Séances de TP :

• TP 1 - (à venir)

• Documents essentiels :

• Aide-mémoire pour la construction de preuves en LEAN (version finale)