Proof assistants for undergraduate mathematics education: elements of an a priori analysis

This paper presents an a priori analysis of the use of six different interactive proof assistants for education, based on the resolution of a typical undergraduate exercise on abstract functions. It proposes to analyse these tools according to several criteria grouped into three categories: language and interaction mode, automation and user assistance and proof structure and visualisation. Our work shows the considerable variability among the selected proof assistants regarding these criteria. We argue that this analysis may help formulate and clarify further research questions on the possible impact of such tools on the development of reasoning and proving skills. In particular, we hypothesise that the choice of a proof assistant entails different effects on the development of memorisation and formulation skills, on the ability to manipulate formal statements and on the perception of the overall structure of a proof.