The word processor that can check your math

Detailed About Page

This page assumes you’ve read the simple introduction on the About page, and it wasn’t enough for you. Here is a deeper introduction to the aim, structure, and design of Lurch.

What is Lurch?

Lurch is a math word processor that checks the steps of the user’s work.

Word processing in Lurch Lite

Word processing (no validation)

What is a step?

A step is any part of a Lurch document (but usually a single mathematical expression) to which a reason is attached (regardless of whether that reason is correct, or even left blank).

What is a reason?

A reason is a reference to a “grading procedure,” a method by which Lurch can check whether the reason justifies the step to which it is attached. Theorems are a common mathematical example of reasons; you cite one, and then the reader (or the software) can check whether you’ve used the theorem correctly. A more computer-oriented example would ask Lurch to use its internal computer algebra system to grade the step of work.

What does it mean to check a step?

“Check” is the informal way to say “validate.” The brains of Lurch is its validation engine.

Simple theorem validated in Lurch

Validating each step of a proof

Different contexts call for different types of validation. Since Lurch is designed for educational use, different learning goals in different courses will dictate different styles of interacting with the program.

Also, there may be varying amounts of validation, from none to very strict.

Can you give some examples?

Before any validation takes place, Lurch is a simple math word processor. Think of Lurch’s word processing core as the trivial example (validation amount equals zero).

But Lurch easy to customize. An instructor can write the theorems and rules he or she wants the students to have access to, and Lurch learns them as the instructor writes them in a document! Students can then cite them by whatever names the instructor gives to them when typing them into the software, and thus they can match the way the instructor or textbook for the course presents the material.

Earlier versions of Lurch used a computer algebra system to validate algebra-based work, but this has been removed when the lack of precision of the systems caused problems.  We are planning ways to re-introduce such validation in future versions.

Lurch validating algebra with its built-in CAS

Validation using a computer algebra system (used in an early release, called Lurch Lite, not currently included in Lurch 0.8)