The Elfe System - Verifying mathematical proofs of undergraduate students
Maximilian Dor\'e, Krysia Broda

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Formal Methods in Verification
