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

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 0 of its 14 references that are in the map.
- First posted on arXiv 8 Feb 2022.

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

- [Improving the Diproche CNL through Autoformalization via Large Language Models](https://mlsanity.com/paper/2303.17513/) (2023)
- [Using Large Language Models for (De-)Formalization and Natural Argumentation Exercises for Beginner's Students](https://mlsanity.com/paper/2304.06186/) (2023)

## Abstract (arXiv)

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.