Introduction

You can use Lurch to check proofs without understanding how it is able to do so. For those of you who want to understand Lurch at a deeper level (or are just curious), here is a very brief high-level overview of how it works.${}^{\ast \ast }$

We answer the question "How does it work?" from three different perspectives: for mathematicians, logicians, and computer scientists.

In what follows we assume you have already read and understand the material in the Quick Start Guides and Writing Proofs worksheet.

Motivation and Goals

One of the main goals of the Lurch project is to check proofs written in the natural mathematical style commonly found in undergraduate textbooks. Let’s identify some key characteristics of that style. Below is a theorem and proof from a randomly selected calculus textbook from my bookshelf.${}^{\ast \ast \ast }$

Notice the following characteristics of such proofs.

• Theorems Are Sentences – The statements being proven are typically written as full sentences containing multiple mathematical expressions rather than a single formal mathematical expression like:
  $$(\mathrm{\forall }x\in (a,b),f^{\prime }(x)=0)\Rightarrow (\mathrm{\exists }c,\mathrm{\forall }x\in (a,b),f(x)=c)$$
• Minimal Justifications – Textbook proofs rarely provide explicit reasons for each step. In the example above, the only justification given is "by the MVT".
• Assumed Context – The proof relies on implicit background material, including previously stated content in the book or unstated prerequisite knowledge expected for the course.
• Informal Logical Notation – Logical symbols such as $\Rightarrow ,\iff ,\vee ,\wedge ,\mathrm{\forall }$, and $\mathrm{\exists }$ are rarely used in such proofs. The example above contains none of them.

Thus, one of the key motivations behind the Lurch validation algorithm is to support checking proofs with these characteristics, written in this informal yet rigorous style. Let’s explore how it achieves that.

Lurch Theory for Mathematicians

If you look at the example proofs in Lurch, one striking feature you may notice is that it does not require that you justify your claims with reasons or explain how you came to any particular conclusion. So how does it determine if your proof is valid?

In simple terms, it begins by considering each statement in your document one at a time and asking "What do we know about this statement?". To answer that question it looks at every definition, theorem, axiom, rule, and formula in the context or document content and checks each one to see if it has anything to say about the particular statement. Whenever it does, it adds the relevant fact to the list of known information. Finally, when all such facts have been determined and collected, it checks if your conclusions follow from the list of known facts.

To convince Lurch, a proof must include sufficient detail to validate each claim. In practice, the only way to convince Lurch that a non-trivial proof correct is if you already know why you are entering each statement. If students only consider one rule at a time to motivate each claim in their proof, then Lurch will find the relevant facts and judge the proof to be valid. But if they skip steps (or have an incorrect proof) Lurch will not be convinced by their argument until they provide more detail and/or correct their mistakes. In this way, students are trained by Lurch to have a justification for every step without explicitly requiring them to do so (just like most proofs in textbooks).

Lurch Theory for Logicians

The goal of Lurch is to be as natural, easy to use, and customizable as possible. Existing proof verification methods and foundations mathematics in the literature (e.g., Formal Axiom Systems, ZFC, Type Theory, Category Theory) are not particularly well-suited for that purpose. This motivates a different approach that is used by Lurch, which we now briefly explain.

A Magic Trick

Think of a topic. Any topic. Don't tell me what it is. Don't even tell me what you think the word 'topic' means. The only requirement is that your topic must have theorems. In fact, don't tell me what you think a 'theorem' is. Without knowing what your topic is, or what you think a theorem is, I will now tell you a true fact about the theorems of your topic:

Either Gina loves mocha is a theorem of your topic, or Gina loves mocha is not a theorem of your topic.

This is true about your topic because it's a tautology, and thus true by definition. In general, any propositional tautology whose atomic propositions are of the form '$t_0$ is a theorem of your topic', '$t_1$ is a theorem of your topic', '$t_2$ is a theorem of your topic', $\dots$ '$t_n$ is a theorem of your topic' will be true about the theorems in whatever topic you might be considering.

How does this help?

• Natural Language Theorems – Modern Foundations of Mathematics like ZFC, Type Theory, Category Theory, frequently begin by defining a language - the set of syntactically valid statements in the mathematical topic that they are trying to formalize.  Lurch's foundation does not make any such restriction. You can define and say whatever you want. Theorems can be environments containing sentences and paragraphs, or a single expression.
• Minimal Justifications – As illustrated in the example above, typical textbook proofs rarely provide explicit reasons for each claim. The Lurch validation algorithm supports this natural style.
• Customizable Context ‐ Lurch does not assume any mathematical or logical rules by default, so instructors and users are free to define their own from scratch. Proofs in undergraduate math textbooks rarely used formal operators like $\Rightarrow$, $\wedge$, $\mathrm{\forall }$, or $\mathrm{\exists }$. Lurch can validate such proofs because it also does not require them (or any other formal operator).
• Propositional Form – Lurch converts your entire document (context, assumptions, theorems and proofs ... all of your meaningful content) to a single proposition, and checks if that proposition is a tautology. You do not have to learn any Lurch-specific rules or reasoning. Yet doing proofs in Lurch 'feels' very natural, as illustrated by the following example.

• (Meta-)True about Everything – As the magic trick above illustrates, the proposition that Lurch actually evaluates is true about whatever topic or model you might be considering. This has some nice implications for context design and development.
  
  

  Recall that any theorem in Neutral Geometry is true about both the Euclidean plane and the hyperbolic plane. Neither Euclid's parallel postulate $E$ nor its negation $\mathrm{\neg }E$ can be proven in Neutral geometry, and either one can be added as an additional axiom without introducing a contradiction. Goedel's Theorem generalizes this situation by showing that for any sufficiently complicated consistent formal system there will always be a statement, $G$, such that neither $G$ nor $\mathrm{\neg }G$ can be proven using that system, and either can be added to the system without introducing a contradiction.
  
  

  From the perspective of the foundation used by Lurch, these results simply say that we can always extend our context to prove results about things that are independent of the context (unless the context allows you to prove everything - the Lurch flavor of 'inconsistent'). This is due to the fact that Lurch does not restrict to a particular formal language or assume any context by default. It allows you to start with any context, spotting whatever high level facts you like, as an alternative to requiring that every proof be built up from very low-level axioms.
  
  

  To illustrate this, consider the following example.

Lurch Theory for Computer Scientists

Validation

Under the hood, Lurch validates your proof using what we call the Global $n$-compact algorithm. A brief overview of the algorithm is given in the talk slides in the first link. A more detailed description, the API documentation, and source code links are after that.

• Validation in Lurch an introduction to the Global $n$-compact validation algorithm used in this version of Lurch (talk slides).
• Validation Algorithm API docs the source code documentation for the Global $n$-compact algorithm and supporting infrastructure.
• Core API docs the LC data structure, putdown notation, matching package, and other core utilties.
• Lurch Web UI docs the code to integrate the Lurch algorithm and core code into the web UI.
• Official Lurch Source Code on GitHub the source code and content of this repository on GitHub.

Parsing

The Lurch web interface uses two parsers written using Peggy. One converts the user's input for meaningful expressions into the internal data structure used by the validation algorithm. The other converts it to the $LATEX$ source needed to render mathematics in the document.

• Lurch Syntax a quick reference showing how to type various math expressions in Lurch.
• 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.