LiberAbaci

Les outils interactifs de preuves sur ordinateur comme le logiciel Coq ont acquis une reconnaissance notable pour la production de logiciels de haute qualité et la vérification de preuves mathématiques complexes.  L'objectif de ce défi est de comprendre comment un outil comme Coq peut faciliter l'enseignement des mathématiques, tout particulièrement pendant les premières années universitaires.  Les questions de recherches de ce projet sont : comment adapter les fondements de la théorie des types ? Comment structurer les connaissances ? Comment rapprocher le langage sur ordinateur et le langage habituel des mathématiques ?  Comment tirer bénéfice de l'automatisation et du calcul pour l’enseignement ? Comment fournir à tous les étudiants un environnement de travail propice à l’apprentissage ?  Comment construire du matériel mathématique approprié et en quantité suffisante pour attirer les enseignants et les étudiants ?  Toutes ces questions devront être étudiées dans le cadre de collaborations avec des enseignants en mathématiques.