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

TL;DR

This paper reports on the deployment of Diproche, a natural language proof checker, in a large introductory mathematics course, highlighting its benefits, student feedback, and potential improvements.

Contribution

It presents first experiences with Diproche in a real classroom setting, demonstrating its practical use and outlining directions for future enhancements.

Findings

Positive student feedback on immediate feedback

Effective detection of proof errors in student solutions

Insights for improving natural language proof checking

Abstract

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.