(MATH 642) | GSÜ - ECTS Guide d'Information

Contenus

Objectif du Cours

Développer une compréhension du formalisme,
Maîtriser les bases de la programmation fonctionnelle,
Être en mesure d'utiliser des assistants de preuve tels
que Lean

Contenu du Cours

Introduction à la programmation fonctionnelle, Types,
Termes, Égalité, Di?érents types, Structures, Classes, Mise en
place de structures mathématiques connues dans Lean,
Preuves de théorèmes connus via Lean

Acquis d'Apprentissage du Cours

Comprendre la nécessité du formalisme en mathématiques,
Apprendre les bases de la programmation fonctionnelle,
Maîtriser l'utilisation des assistants de preuve

Méthodes d'Enseignement

En présentiel ou en ligne

Ressources

How To Prove It (with Lean), Daniel J. Velleman
Theorem Proving in Lean 4, Jeremy Avigad, Leonardo de Moura, Soonho Kong, and Sebastian Ullrich,

Intitulés des Sujets

Intitulés des Sujets Théoriques
Semaine	Intitulés des Sujets
1	Présentation et installation
2	Syntaxe Lean et interface de preuve
3	Rappel de logique dans Lean
4	Tactiques et style de preuve
5	Structures et classes de types
6	Types inductifs et récursion
7	Preuves par recurrence
8	Ensembles et relations
9	Hiérarchie algébrique
10	Théorie des nombres dans Lean I
11	Théorie des nombres dans Lean II
12	Structures finies et combinatoire I
13	Structures finies et combinatoire II
14	Analyse dans R

Intitulés des Sujets Pratiques
Semaine	Intitulés des Sujets
1	---
2	---
3	---
4	---
5	---
6	---
7	---
8	---
9	---
10	---
11	---
12	---
13	---
14	---

Système d'évalution

Contribution à la Note Finale
Activités	Numéro	Contribution
Contribution du contrôle continu à la note finale	4	60
Contribution de l'examen final à la note finale	1	40
Total	5	100

Contrôle Continu
Activités	Numéro	Contribution
Devoir	0	0
Présentation	3	45
Examen partiel (temps de préparation inclu)	0	0
Projet	1	15
Travail de laboratoire	0	0
Autres travaux pratiques	0	0
Quiz	0	0
Devoir/projet de session	0	0
Portefeuille	0	0
Rapport	0	0
Journal d'apprentissage	0	0
Mémoire/projet de fin d'études	0	0
Séminaire	0	0
Autre	0	0
Make-up	0	0
Total	4	60

Evalution de la Compétence

No	Objectifs Pédagogiques du Programme	Contribiton
No	Objectifs Pédagogiques du Programme	1	2	3	4	5
1					X
2						X
3						X
4						X
5					X
6						X
7				X
8		X
9			X
10		X

Tableau de la Charge de Travail

Activités	Nombre	Durée	Charge totale de Travail
Durée du cours	14	3	42
Préparation pour le cours	14	5	70
Devoir	0	0	0
Présentation	3	8	24
Examen partiel (temps de préparation inclu)	0	0	0
Projet	1	10	10
Laboratoire	0	0	0
Autres travaux pratiques	0	0	0
Examen final (temps de préparation inclu)	1	36	36
Quiz	0	0	0
Devoir/projet de session	0	0	0
Portefeuille	0	0	0
Rapport	0	0	0
Journal d'apprentissage	0	0	0
Mémoire/projet de fin d'études	0	0	0
Séminaire	0	0	0
Autre	0	0	0
baclé	0	0	0
Yil	0	0	0
Yil	0	0	0
Yil	0	0	0
Charge totale de Travail			182
Charge totale de Travail / 25			7.28
Crédits ECTS			7

Semaine	Intitulés des Sujets
1	---
2	---
3	---
4	---
5	---
6	---
7	---
8	---
9	---
10	---
11	---
12	---
13	---
14	---

Semaine	Intitulés des Sujets
1	---
2	---
3	---
4	---
5	---
6	---
7	---
8	---
9	---
10	---
11	---
12	---
13	---
14	---

Semaine	Intitulés des Sujets
1	---
2	---
3	---
4	---
5	---
6	---
7	---
8	---
9	---
10	---
11	---
12	---
13	---
14	---