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 matin
Page dédiée à la tâche

Mettre à jour cette page

Les instructions sont disponibles ici.