Number Theory and Axiomatic Geometry in the Diproche System

TL;DR

Diproche is an automated proof checking system designed to support beginners in learning elementary mathematics proofs through controlled natural language, focusing on number theory and axiomatic geometry.

Contribution

The paper introduces the architecture and key features of Diproche, a novel proof checker tailored for didactical purposes in elementary number theory and geometry.

Findings

Effective proof verification in controlled natural language

Adaptability to different educational levels and topics

Supports learning in elementary number theory and geometry

Abstract

Diproche ("Didactical Proof Checking") is an automatic system for supporting the acquistion of elementary proving skills in the initial phase of university education in mathematics. A key feature of Diproche - which is designed by the example of the Naproche system developed by M. Cramer and others - is an automated proof checker for proofs written in a controlled fragment of natural language specifically designed to capture the language of beginners' proving exercises in mathematics. Both the accepted language and proof methods depend on the didactical and mathematical context and vary with the level of education and the topic proposed. An overall presentation of the system in general was given in Carl and Krapf 2019. Here, we briefly recall the basic architecture of Diproche and then focus on explaining key features and the working principles of Diproche in the sample topics of elementary number theory and axiomatic geometry.