Ce projet propose des ressources et outils pour faciliter l'enseignement des mathématiques à travers des travaux dirigés utilisant l'assistant de preuve Coq. Il inclut des documents pédagogiques, des maquettes d'interfaces interactives, des prototypes logiciels et des expérimentations menées avec des élèves pour améliorer l'apprentissage des concepts mathématiques et logiques.