Using Automated Theorem Provers for Mistake Diagnosis in the Didactics of Mathematics

The Diproche system, an automated proof checker for natural language proofs specifically adapted to the context of exercises for beginner's students similar to the Naproche system by Koepke, Schröder, Cramer and others, uses a modification of an automated theorem prover which uses common formal fallacies intead of sound deduction rules for mistake diagnosis. We briefly describe the concept of such an'Anti-ATP' and explain the basic techniques used in its implementation. Learning how to prove is one major obstacle of the introductory phase of university education in mathematics. It requires practice, i.e. exercises, which need to be corrected, which is both an expensive and time-consuming task. This limits the way in which corrections can usually enter into the process of solving proof exercises as feedback.