Automatized Evaluation of Formalization Exercises in Mathematics

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