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 :

• 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

• Diaporama de la seconde séance

• Séances de TP :

• TP 1

• TP 2

• TP 3

• TP 4

• TP 5

• TP 6

• TP 7

• TP 8 (feuille de résultats auxiliaires : Resultats_elementaires_analyse.lean)

• Documents essentiels :

• Aide-mémoire pour la construction de preuves en LEAN