for the learning of mathematics

an international journal of mathematics education

Gila Hanna ,  Xiaoheng Yan - Vol. 41 Num. 3 (2021)
 Opening a discussion on teaching proof with automated theorem provers


The paper argues that there is a need for new approaches to teaching proof with newly-available technology. It contributes to filling this need by opening a discussion on digital proof assistants, programs that allow one to do mathematics with the aid of a computer, construct proofs, and check their correctness. The paper starts by exploring such proof assistants, then argues that they could play an important role in fostering students’ appreciation and understanding of proof and of mathematics. Finally, the paper points out the need to develop explicit pedagogic strategies tailored to assist teachers in deploying such computer-based tools.