Lurch Resources

Reference, installation, source code, talks, and advanced tools

Most people should begin with Getting Started, the Introduction to Proof, or Practice Proofs with Lurch. This page collects more specialized links for instructors, developers, and advanced users.

Quick-start guides short interactive documents for students and instructors.
Lurch Syntax a quick reference for typing mathematical expressions in Lurch.
Course contexts and rule documents the contexts used by the Introduction to Proof notes with links to the relevant chapters. Additional contexts can be found on the Getting Started page.
Lurch Design and Theory a high-level explanation of the validation approach behind Lurch.
Validation in Lurch (slides) talk slides about the super-natural deduction validation algorithm.
Introduction to Lurch Plus (slides) slides from a recent talk on Lurch Plus.

Start Lurch open a blank document with one of several common mathematical contexts.
Instructor file-handling notes background on static contexts, dynamic contexts, and browser restrictions.
Install or customize Lurch instructions for installing Lurch as an app, or customizing obtaining your own copy of Lurch and this site.
Install Lurch locally a brief guide for hosting a local copy of this site on your own computer. Mainly for developers.

Changelog recent changes and updates to the Lurch app and site.
Official Lurch source code on GitHub the source code and content for this repository.
Validation Algorithm the code-level nitty gritty documentation for the implementation of the Lurch validation algorithm.
Lurch Concepts the data structure and utilities used by Lurch to formalize mathematics. Also called Logic Concepts in the code.
Peggy LaTeX Parser Grammar this is the full Peggy source code for the tex parser.
Peggy Putdown Parser Grammar this is corresponding Peggy source code for the putdown parser.