Abstract

According to a widely held view, mathematical proofs are essentially (indications of) formal derivations, and thus in principle mechanically checkable (this view is defended, for example, by Azzouni [3]). This should in particular hold for the kind of simple proof exercises typically given to students of mathematics learning to write proofs. If that is so, then automated proof checking should be an attractive option for math education at the undergraduate level. An opposing view would be that mathematical proofs are social objects and that what constitutes a mathematical proof can thus not be separated from the social context in which it arises. In particular, such “sociomathematical norms” play a role in teaching situations, see, for example, Stephan [37]. There thus seems to be a tension between the inherent social nature of “natural” mathematical proofs and attempts at their automated verification. In this paper, we explore this tension both theoretically and on the basis of our experiences with developing the Diproche system, a program for the automated verification of natural language proofs in college-level introduction to proof classes (modelled after the example of the Naproche system by Cramer, Koepke et al. [14]) and its use at the Europa-Universität Flensburg during the winter term 2020/2021.