Home Tutorial Examples Source

∈ ∩ ∪ ⊆ ᑦ -> ∘ ⁻¹ [ ] { }

Line , Col

Interactive Theorem Proving for Students

This tool is meant for students to practice writing mathematical proofs. Several background libraries for sets, relations and functions have been implemented such that you can directly start writing a proof.

To get started, you best take a look at the tutorial and the examples

How does it work?

Internally, the mathematical text is transformed into a sequence of first-order formulas. This representation implies certain proof obligations which are checked by Automated Theorem Provers. An overview of the inner workings is described in a preprint which will be presented at CSEDU 2018. A complete system description can be found here.

The tool itself is written in Haskell. If you want to learn more about the implementation, have a look at the source code.

Get involved

You want to improve Elfe or implement new background libraries? You can get in touch via GitHub. If you want to do a larger project with Elfe, e.g., work on it in your thesis, you best get in touch with us at dev@elfe-prover.org.