Technology-supported learning of proof in mathematics

Cabri-Euclide, Luengo, 2005

Proof assistants, an automatic theorem proving research track, are reaching a maturity which suggests that is possible to the exploration of their use for the learning of proof in  mathematics first at the level of higher education and at tentatively the upper secondary school. 

It in the context of this pioneer research that is organised the PAT 2023 Thematic School which seeks to offer a broad spectrum of current research in the field of didactic of proof, the impact of the use of proof assistants in education, formalization of mathematics and user interfaces for theorem proving. I will give a lecture which will include  (1) a survey of the evolution of AI research on the learning of proof in mathematics, (2) lessons learned from the past focusing on the relations between reasoning-proving and knowledge representation, and on the problem of feedback, eventually (3) didactic analysis of the teaching of mathematical proof and its implications for the design of learning environments. The introduction will outline the history of the teaching of proof in mathematics, a short epilogue will raise epistemological issues.

Suggested readings:

Arzarello, F. (2007). The proof in the 20th century (From Hilbert to Automatic Theorem Proving Introduction). In P. Boero (Éd.), Theorems in School : From History, Epistemology and Cognition to Classroom Practice (p. 43‑63). BRILL.
Balacheff, N. (2023). Notes for a study of the didactic transposition of mathematical proof. Philosophy of Mathematics Education Journal, 2023 volume
Balacheff, N., & Boy de la Tour, T. (2019). Proof Technology and Learning in Mathematics : Common Issues and Perspectives. In G. Hanna, D. Reid, & M. de Villiers (Éds.), Proof Technology in Mathematics Research and Teaching. Springer.
Czocher, J. A., & Weber, K. (2020). Proof as a Cluster Category. Journal for Research in Mathematics Education, 51(1), 50‑74.
Hanna, G., & Xiaoheng, (Kitty) Yan. (2021). Opening a discussion on teaching proof with automated theorem provers. For the Learning of Mathematics, 41(3), 42‑46.
Luengo, V. (2005). Some didactical and Epistemological Considerations in the Design of Educational Software : The Cabri-euclide Example. International Journal of Computers for Mathematical Learning, 10(1), 1‑29.