Input a proof in plain English in the web interface, and recieve immediate feedback on whether it is right or not, and how to fix it!
- Provides convenient interface for authoring proofs, including buttons for special characters
- Recieve feedback on where in the proof you're wrong if there are any mistakes
- Useful for:
- Checking whether your homework is correct
- Automatically grade tests/exams without human intervention
- Writing informal proofs while still checking for correctness
- Grades set theory based proofs
- Automatically identifies variables, sets, claims and assumptions in a proof
- Transpiles using NLP techniques to Lean, a programming language meant for proof checking
- Simply type your formatted proof into the box and hit submit to get your proof checked!
- Install lean from the official website
- Set the
LEAN_PATH_PRAIRIEenvironment variable to the path of theleanexecutable - Clone this repository into a folder
- Create a python virtualenv and install the python dependencies with
pip -r requirements.txt - Run the server with
python proof.py - Visit the url as specified in the flask console output.
- http://flask.pocoo.org/docs/1.0/
- http://alan.blog-city.com/jquerylinedtextarea.htm
- https://leanprover.github.io/documentation/
Licensed under AGPL v3.0. For more details, visit LICENSE