Natural Language Proof Checking in Introduction to Proof Classes – First Experiences with Diproche

Merlin Carl
(Europa-Universität Flensburg)
Hinrich Lorenzen
(Europa-Universität Flensburg)
Michael Schmitz
(Europa-Universität Flensburg)

We present and analyze the employment of the Diproche system, a natural language proof checker, within a one-semester mathematics beginners lecture with 228 participants. The system is used to check the students' solution attempts to proving exercises in Boolean set theory and elementary number theory and to give them immediate feedback. The benefits of the employment of the system are assessed via a questionnaire at the end of the semester and via analyzing the solution attempts of a subgroup of the students. Based on our results we develop approaches for future improvements.

In João Marcos, Walther Neuper and Pedro Quaresma: Proceedings 10th International Workshop on Theorem Proving Components for Educational Software (ThEdu'21), (Remote) Carnegie Mellon University, Pittsburgh, PA, United States, 11 July 2021, Electronic Proceedings in Theoretical Computer Science 354, pp. 59–70.
Published: 8th February 2022.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: