LiberAbaci
Enseigner les mathématiques à l'aide de Coq
LiberAbaci est un projet collaboratif visant à améliorer
l'accessibilité du système de preuve interactif Coq pour un
public d'étudiants en mathématiques dans les premières années
universitaires.
Evénements et résultats notables
Réunion de lancement
La réunion de lancement a eu lieu le 20 septembre 2022 dans les
locaux de l'Inria Paris. Le programme
de cette réunion permet
d'avoir accès aux présentations qui ont été faites.
Tâches
Tâche 1 : Collaborations avec des enseignants
Nous cherchons à établir des contacts avec des enseignants en mathématique et des chercheurs en didactique.
Page dédiée
Tâche 2 : Fondements de la théorie des types
Tâche 3 : Structures, inférence et hiérarchies
Tâche 4 : Notations extensibles et langage de surface
Cette tâche cherche à expérimenter de nouveaux mécanismes de notations et de langage de preuve,
afin de se rapprocher autant que possible des notations usuelles dans un cours de mathématique.
Page dédiée
Tâche 5 : Traitements automatiques
Tâche 6 : Environnements interactifs
Tâche 7 : Création de bibliothèque sur des domaines
précis
Le but est de disposer d'une collection de
bibliothèques thématiques motivée par le besoin d’enseignement, dont
algèbre, analyse par exemple intégrale de Lebesgue, arithmétique
par exemple divisibilité...
Réunion (en visio) le 11 décembre au matinPage
dédiée à la tâche
Mettre à jour cette page
Les instructions sont
disponibles ici.