Automatized Evaluation of Formalization Exercises in Mathematics

TL;DR

This paper introduces two automated systems to support beginners in learning formal logic and geometric pattern formalization through interactive exercises with immediate feedback.

Contribution

It presents novel systems for automatic evaluation of formalization exercises in mathematics, combining natural language and geometric pattern formalization tasks.

Findings

Effective automatic checking of formalization exercises

Supports beginner students in learning formal logic and geometry

Enhances learning through immediate feedback

Abstract

We describe two systems for supporting beginner students in acquiring basic skills in expressing statements in the formalism of first-order predicate logic; the first, called "math dictations", presents users with the task of formalizing a given natural-language sentence, while the second, called "Game of Def", challenges users to give a formal description of a set of a geometric pattern displayed to them. In both cases, an automatic checking takes place.