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.

We tell Lurch which symbols our mathematical system requires like this: `Declare and, or, implies, not`. **Conjunction introduction:** `If A` and `if B` then we can conclude `A and B`. **Conjunction elimination:** `If A and B` then we can conclude `A` and separately conclude `B`. **Disjunction introduction:** `If A` then we can conclude `A or B`, conclude `B or A`, or even both. **Disjunction elimination:** (Version 1) `If A or B` and `not A` then it must be `B`. (Version 2) `If A or B` and `not B` then it must be `A`. **Conditional introduction:** To prove a conditional, we must construct a subproof of the following form. `Assume A`. Then, typically after some work, prove `B`. From that subproof, we can conclude `A implies B`. **Conditional elimination:** `If A implies B` and `if A`, then we can conclude `B`. **Negation introduction:** If we start a subproof with "`assume A`" and we end it with a contradiction, say `B` and `not B`, then we can end the subproof... ...and conclude `not A`. **Negation elimination:** If we start a subproof with "`assume not A`" and we end it with a contradiction, say `B` and `not B`, then we can end the subproof... ...and conclude `A`.
**Contrapositive:** `If X implies Y` then `not Y implies not X`. `Assume X implies Y`. To establish the contrapositive, we must use a subproof. `Assume not Y`. The easiest way to show $\neg X$ is with an inner subproof. `Assume X`. Then we can apply the original assumption to conclude `Y`, but we already know that `not Y` is true. That's a contradiction. So outside that inner subproof, we can conclude `not X`. Since we assumed $\neg Y$ and proved $\neg X$ from it, we can conclude `not Y implies not X`.

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