We describe two systems that use text-davinci-003, a large language model, for the automatized correction of (i) exercises in translating back and forth between natural language and the languages of propositional logic and first-order predicate logic and (ii) exercises in writing simple arguments in natural language in non-mathematical scenarios.

The Diproche system is an automated proof checker for texts written in a controlled fragment of German, designed for didactical applications in classes introducing students to proofs for the first time. The first version of the system used a controlled natural language for which a Prolog formalization routine was written. In this paper, we explore the possibility of prompting large language models for autoformalization in the context of Diproche, with encouraging first results.

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.

Learning the correct use of mathematical language frequently poses a challenge for beginner students. At the same time, it is a basic skill, required both for understanding mathematical texts and for presenting one's own work. In mathematical lectures and typical textbooks, this is rarely explictly discusses, though some offer a brief discussion, along with some formalization exercises (see, e.g., [Ha]). In this note, we present two pieces of software that pursue the goal to support beginner students in learning the use of formal language. The first one, called "Math Dictations" (a word that we learned from M. Junk, who used the concept (but no automatization thereof) in introductory courses at the university of Konstanz), challenges students to translate a proposition given in natural language, such as "the real function f is strictly increasing" into a quantifier formula such as x y(x y f(x) f(y)). It is similar to the formalization exercises that form part of the "Mathematical Logic Tutor" by A. Moreno (see [BM]), but goes beyond this in (i) allowing first-order logic rather than propositional logic and (ii) using a restricted automated theorem prover for evaluating solutions, so that many solutions, rather than a single one, are recognized as correct answers. After the "Math Dictations" had been implemented and the first version of this article had been posted, we were made aware of the fact that this kind of formalization exercise is available in the Edukera system