Maths with Coq in L1, a pedagogical experiment
Marie Kerjean, Micaela Mayero, Pierre Rousselin
TL;DR
The paper examines an 18-hour, hands-on Coq-based course for first-year L1 students in mathematics and computer science, designed to teach formal proofs across propositional logic, natural numbers, predicate calculus, and real numbers. It documents practical worksheets, pedagogical strategies, and iterative improvements, while candidly reporting difficulties encountered, such as managing forward versus backward reasoning and classroom pacing. Key contributions include a detailed account of design choices, student engagement factors, assessment approaches, and a critical evaluation of Coq's tooling and interfaces in an educational setting. The work demonstrates the feasibility and challenges of early formal-methods education with a minimal, bare-bones Coq workflow and offers concrete directions for pedagogy and tooling improvements to enhance learning outcomes and measurement of mathematical understanding.
Abstract
In France, the first year of study at university is usually abbreviated L1 (for premiere annee de Licence). At Sorbonne Paris Nord University, we have been teaching an 18 hour introductory course in formal proofs to L1 students for 3 years. These students are in a double major mathematics and computer science curriculum. The course is mandatory and consists only of hands-on sessions with the Coq proof assistant. We present some of the practical sessions worksheets, the methodology we used to write them and some of the pitfalls we encountered. Finally we discuss how this course evolved over the years and will see that there is room for improvement in many different technical and pedagogical aspects.