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

arXiv: https://arxiv.org/abs/2002.05083 · HTML: https://mlsanity.com/paper/2002.05083/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 12 Feb 2020.

## Built on by (most cited first, 1 of 1)

- [Using Large Language Models for (De-)Formalization and Natural Argumentation Exercises for Beginner's Students](https://mlsanity.com/paper/2304.06186/) (2023)

## Abstract (arXiv)

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"oder, 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.