Résumé
This paper presents an a-priori analysis of the use of five 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 three main categories of aspects: language and interaction mode, automation and user assistance, and proof structure and visualisation. 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.