Structures mathématiques et formalisation(MAT440)
| Nom du Cours | Semestre du Cours | Cours Théoriques | Travaux Dirigés (TD) | Travaux Pratiques (TP) | Crédit du Cours | ECTS | |
|---|---|---|---|---|---|---|---|
| MAT440 | Structures mathématiques et formalisation | 7 | 3 | 0 | 0 | 3 | 5 |
| Cours Pré-Requis | |
| Conditions d'Admission au Cours |
| Langue du Cours | |
| Type de Cours | Électif |
| Niveau du Cours | Licence |
| Enseignant(s) du Cours | Ayberk ZEYTİN azeytin@gsu.edu.tr (Email) |
| Assistant(e)s du Cours | |
| 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 |
| Contenus |
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 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 | --- |
Contribution à la Note Finale
| Numéro | Frais de Scolarité | |
|---|---|---|
| Contribution du contrôle continu à la note finale | 6 | 60 |
| Contribution de l'examen final à la note finale | 1 | 40 |
| Toplam | 7 | 100 |
Contrôle Continu
| Numéro | Frais de Scolarité | |
|---|---|---|
| Devoir | 0 | 0 |
| Présentation | 6 | 60 |
| Examen partiel (temps de préparation inclu) | 0 | 0 |
| Projet | 0 | 0 |
| 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 |
| Toplam | 6 | 60 |
| No | Objectifs Pédagogiques du Programme | Contribiton | ||||
|---|---|---|---|---|---|---|
| 1 | 2 | 3 | 4 | 5 | ||
| Activités | Nombre | Durée | Charge totale de Travail |
|---|---|---|---|
| Durée du cours | 14 | 3 | 42 |
| Préparation pour le cours | 14 | 3 | 42 |
| Devoir | 0 | 0 | 0 |
| Présentation | 3 | 5 | 15 |
| Examen partiel (temps de préparation inclu) | 0 | 0 | 0 |
| Projet | 0 | 0 | 0 |
| 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 | 135 | ||
| Charge totale de Travail / 25 | 5.40 | ||
| Crédits ECTS | 5 | ||