The Lurch Project
Lurch is a word processor designed to check the reasoning in proofs, specifically the types of proofs that students do in an introduction to proofs course.
Its purpose is to give immediate and helpful feedback about whether a student is doing their proof correctly, so that the student learns the mechanics and rules of proof writing more quickly and thoroughly than if they had to wait days for manually graded feedback.
Current status
The latest version of Lurch is a web application that is in alpha testing at the moment. You can try it online here! A simple example proof in propositional logic is shown below.
Documentation
Warning
We are just beginning to write documentation, but you can find a tutorial online here. New bug fixes, new features, and new documentation arrive almost every day. Expect a more stable release in late spring of 2024.
Potential new contributors can check out the new app's GitHub repository here.
Other tools
- The Lurch Deductive Engine (LDE) is the set of data structures and algorithms used under the hood to validate proofs
- We may later incorporate this JavaScript implementation of the Earley parsing algorithm to allow users to customize the notation used in the app, but that remains uncertain.
- Old versions of our work are archived here.