The Elfe System - Verifying mathematical proofs of undergraduate students

TL;DR

Elfe is an interactive system that helps undergraduate students learn basic proof methods in discrete mathematics by converting natural language inputs into formal formulas and verifying proof obligations with automated theorem provers.

Contribution

This paper introduces Elfe, a novel system combining natural language processing and automated theorem proving to assist students in understanding proofs in discrete mathematics.

Findings

Successfully tested with undergraduate students

Supports proof verification through automated theorem provers

Provides an accessible web and command-line interface

Abstract

Elfe is an interactive system for teaching basic proof methods in discrete mathematics. The user inputs a mathematical text written in fair English which is converted to a special data-structure of first-order formulas. Certain proof obligations implied by this intermediate representation are checked by automated theorem provers which try to either prove the obligations or find countermodels if an obligation is wrong. The result of the verification process is then returned to the user. Elfe is implemented in Haskell and can be accessed via a reactive web interface or from the command line. Background libraries for sets, relations and functions have been developed. It has been tested by students in the beginning of their mathematical studies.