Proof assistants in mathematics learning - Appraising, Analyzing, Designing, Experimenting, Assessing – APPAM

Proof is epistemologically the fundamental constituent of any mathematical activity. At all levels of schooling and training, it contributes to the process of learning mathematical knowledge. Thanks to the perspective brought by Technology Enhanced Learning (TEL), the international research on technologies in mathematics learning points out the necessity of a multidisciplinary structuring of work to analyze the uses and the benefits of proof assistants (called PA) in the learning of proof. Proof assistants, used by mathematicians, are free open-source software that check a proof.
This project aims to fill the gap in research in France on the learning of proof, which remains problematic at the transition from secondary to higher education. It proposes a multidisciplinary approach, combining tools, results and methods from sciences (mathematics and computer science) and from social and human sciences (didactics). The aim is to develop and evaluate a new approach to teaching proof based on the adaptation and the integration of PA at the beginning of university. Three objectives structure this project: to characterize the difficulties of learners and the existing uses of PA in France; to analyze AP in a learning perspective; to experiment and evaluate the benefits of PA at the beginning of university in mathematics learning. The methods used to achieve these objectives mobilize internationally validated epistemological, didactic, and cognitive frameworks on proof and proving, and articulate quantitative and qualitative approaches.
The results of this project will inform researchers, teachers, trainers, and educational policy makers about: high school and college students' difficulties with proof, uses and adaptations of PA for educational purposes, evaluation of PA benefits in learning, and didactic recommendations for the teaching and learning of proof in high school and university.