(209) 460-7934
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 2047000088 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 4372267676 which will be presented at 8506036648. A complete system description can be found 867-219-5733.

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 5705071173. 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.