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

• Documents essentiels :

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

• Séances de TP :

• TP 1

• TP 2

• TP 3

• TP 4

• TP 5

• TP 6

• TP 7

• TP 8

• Sujets d'examen :

• Examen 2024-2025

• Grille pour l'examen