Proof Verification with Lurch

Building the bridge to higher mathematics

Is my proof correct?
Lurch says it is not convinced.
I need to say more.

Anonymous, 2024

Lurch is a math editor that can check your proofs (coauthored with Nathan Carter). It was used successfully in my four credit undergraduate bridge course for math and math education majors. Instructors who would like to create their own Lurch course materials using the rule libraries and content from my course can find updated and improved supporting materials below and on this site.

Documentation and Examples

  • Introductory Worksheets
  • Examples – a few proofs done in Lurch using the topics defined below.
    • Example Proofs - a sample of some proofs in Lurch using a variety of topics and styles.
    • Double induction - a proof of a binomial coefficient identity done in class using double induction (and the recursive definition of binomial coefficients given in the course). Colored fonts are used to help keep track of which induction is which.
    • Topo-logical - a proof that the composition of continuous functions is continuous in Topology. (spoiler alert: this is the solution to part D of the Final Exam below)
    • 100 Famous Theorems Challenge! - Lurch's status in verifying the proofs of theorems on the 100 famous theorems challenge list. Game on!
  • Final Exam! - try your hand at the Math 299 Final Exam from Spring 2024 (four parts)
  • Lurch Deductive Engine– the nitty gritty details under the hood of the validation algorithm used by the Lurch Deductive Engine for developers (not up to date, but mostly correct)
    • Validation in Lurch - introduction to the Global $n$-compact validation algorithm used in this version of Lurch.
    • 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
    • Source Repo on GitHub - the source code and content of this repository on GitHub
  • Lurch Syntax – a quick reference showing how to type various math expressions in Lurch
  • Math 299 Home Page – for my Introduction to Mathematical Proof course at the University of Scranton, Spring 2024.

Math 299 Lurch Rule Libraries

Cumulative Topics – each link one opens a blank Lurch document whose context consists of the rules for that topic, and those from the topics above it. The Theorem numbers refer to exercises in the draft of the course lecture notes.

Propositional Logic
defines and, or, not, implies, iff, and contradiction (view rules)
Predicate Logic with Equality
defines forall $\left(\forall\right)$, exists $\left(\exists\right)$, equality $\left(=\right)$, unique existence $\left(\exists!\right)$ (view rules)
Logic Theorems
provides some common theorems from Logic (view rules)
Natural Numbers
the Peano Axioms for the Natural Numbers (view rules)
Number Theory Definitions
defines, less than $\left(\lt\right)$, divides $\left(\mid\right)$, prime, even, odd (view rules)
Equations
defines a single ‘rule’ that enables Lurch to validate transitive chains of equalities without needing substitution, reflexivity, symmetry, or transitivity (view rules)
Number Theory Theorems
provides some useful theorems from Number Theory that are provable from the Peano Axioms (view rules)
Sequences and Recursion
defines summation $\left(\sum\right)$, Fibonnaci numbers $\left(F_n\right)$, factorial $\left(!\right)$, multinomial coefficients $\binom{n}{k}$, binomial coefficients, exponentiation $\left(z^n\right)$ (view rules)
Real Numbers
defines the field axioms for the Real Numbers (view rules)
Set Theory
defines in $\left(\in\right)$, subset $\left(\subseteq\right)$, intersection $\left(\cap\right)$, union $\left(\cup\right)$, complement $\left(‘\right)$, set difference $\left(\setminus\right)$, powerset $\left(\mathscr{P}\right)$, Cartesian product $\left(\times\right)$, finite set $\left(\{ \ldots \}\right)$, tuple $\langle\ldots\rangle$, Indexed Union $\left(\bigcup\right)$, Indexed Intersection $\left(\bigcap\right)$, Set Builder notation $\left(\{ z : \ldots\}\right)$ (view rules)
Functions
defines maps $\left(f\colon A \to B\right)$, function application $\left(f(x)\right)$, maps to $\left(\mapsto\right)$, image $\left(f(U)\right)$, identity map $\left(\text{id}_A\right)$ inverse image $\left(f^\text{inv}(U)\right)$, composition $\left(\circ\right)$, inverse function $\left(f^{-1}\right)$, injective, surjective, bijective (view rules)
Relations
defines reflexive, symmetric, transitive, irreflexive, antisymmetric, total, partial order, strict partial order, total order, equivalence relation, partition, equivalence class $[a]$ (view rules)

Other Useful Contexts

Additional Rules. The following rules can be optionally added by the instructor to any context above in a particular document. Currently, only one of the three Arithmetic rules can be used in a single document.

Arithmetic in the Natural Numbers
Allows the user to say by arithmetic after an expression to try to justify it using a CAS. The expression can only contain natural number constants (e.g. $0$, $1$, $2$, etc) the operators $+$, $\cdot$, and $\text{^}$, and the relations $=$, $\leq$, and $\lt$. (view rules)
Arithmetic in the Integers
Allows the user to say by arithmetic after an expression to try to justify it using a CAS. The expression can only contain natural number constants (e.g. $0$, $1$, $2$, etc) the operators $+$, $\cdot$, $\text{^}$, and $-$ and the relations $=$, $\leq$, and $\lt$. Exponents cannot be negative. (view rules)
Arithmetic in the Rationals
Allows the user to say by arithmetic after an expression to try to justify it using a CAS. The expression can only contain natural number constants (e.g. $0$, $1$, $2$, etc) the operators $+$, $\cdot$, $\text{^}$, $-$, and $/$, and the relations $=$, $\leq$, and $\lt$. Exponents must be integers and you cannot divide by zero. (view rules)
Algebra
Allows the user to say by algebra after any (binary) equation to try to justify it using a CAS. There are no restrictions on what the expression can contain, so use at your own discretion. The identity is evaluated using Algebrite. (view rules)

Useful Cumulative Contexts. These contexts combine some proper subsets of the cumulative Math 299 contexts listed above.

Equations and Logic Only
Equations, Logic Theorems, Predicate Logic, Propositional Logic.
Sets, Equations, and Logic
Set Theory, Equations, Logic Theorems, Predicate Logic, Propositional Logic. This does not include Set Theory Theorems.
Functions, Sets, Equations, and Logic
Functions, Set Theory Theorems, Set Theory, Equations, Logic Theorems, Predicate Logic, Propositional Logic.
Topology
Defines topological space, open, closed, and continuous (in a toplogical space). Includes the Functions library above. (view rules)

Example Assignments

Math 299 Spring 2024 Assignments – each link one opens a Lurch document containing a homework assignment from the course. Note that Lurch was under development during this semester so that some assignments are not good examples of what can be done today if these were rewritten to take advantage of some of the new features. We are in the process of updating them. I also intend to revise the entire syllabus in like of having Lurch available to spend less time on formal logic and more time on the later topics in the course (and perhaps add a few new ones).

The theorem numbers for the assigned problems below refer to the following course lecture notes. These are not fully updated to be consistent with the libraries used in the assignments below and may be revised frequently.

Lecture Notes

Assignment #06Propositional logic
  1. Theorem (Iff is stronger):$(P\Leftrightarrow Q)\Rightarrow(Q\Rightarrow P)$
  2. Theorem (the other way around):$\neg(\neg A)\Rightarrow A$
  3. Theorem (Modus Tollens):$(S \Rightarrow T)\text{ and } \neg T \Rightarrow \neg S$
  4. Theorem (atomic statements don't have to be variables):$0 \lt x\text{ or }x\lt 10 \Rightarrow x\lt 10\text{ or } 0\lt x$
  5. Theorem (excluded middle):$K\text{ or } \neg K$
Assignment #07Propositional logic
  1. Theorem (implies is transitive):$((P\Rightarrow Q)\text{ and }(Q \Rightarrow R)) \Rightarrow (P \Rightarrow R)$
  2. Theorem (alternate or-):$(S\text{ or } T)\text{ and } \neg S \Rightarrow T$
Assignment #08Predicate logic with Equality
  1. Theorem (alpha equivalence warm up):$(\forall x.P(x)) \Rightarrow (\forall y.P(y))$
  2. Theorem (same thing but for exists):$(\exists x.P(x)) \Rightarrow (\exists y.P(y))$
  3. Theorem (commuting quantifiers):$(\forall x.\forall y.x\text{ loves }y) \Rightarrow (\forall y.\forall x.x\text{ loves }y)$
  4. Theorem (same thing for exists):$(\exists x.\exists y.x\text{ loves }y) \Rightarrow (\exists y.\exists x.x\text{ loves }y)$
  5. Theorem (DeMorgan):$\neg (S\text{ and }T) \Rightarrow \neg S\text{ or } \neg T$
  6. Theorem (DeMorgan):$\neg (\forall x.R(x)) \Rightarrow (\exists x.\neg R(x))$
  7. Theorem ($=$ is transitive):$x=y\text{ and }y=z \Rightarrow x=z$
Assignment #09Logic theorems
  1. Theorem 5.10 (some are the same):$(\forall x.\forall y.P(x,y)) \Rightarrow (\forall z.P(z,z))$
  2. Theorem 5.16 (excluded middle):$(\forall x.Q(x))\text{ or } (\exists x.\neg Q(x))$
  3. Theorem 4.22 (alternate $\Rightarrow$):$(R \Rightarrow S) \Rightarrow \neg R\text{ or }S$
Assignment #10Logic review
  1. Theorem (ex falso quodlibet):If Dracula fears Alice and Dracula does not fear Alice then Bob loves Alice.
  2. Theorem 4.29 (the most beautiful?):$S \Rightarrow (S \Leftrightarrow S\text{ or }(\neg S \text{ and } S))$
  3. Theorem 4.25 (shunting):$((P \text{ and } Q) \Rightarrow R) \Leftrightarrow (P \Rightarrow (Q \Rightarrow R))$
  4. Theorem 5.21 (avoiding vacuous domains):$(\exists x. x = x)\text{ and }(\forall y. T(y)) \Rightarrow (\exists z. T(z))$
  5. Theorem 5.5 (distributivity):$(\exists x. A(x) \Rightarrow B(x)) \Leftrightarrow (\forall y. A(y)) \Rightarrow (\exists z. B(z))$
Assignment #11Logic review
  1. Theorem (Pierce's Law)$((S \Rightarrow T) \Rightarrow S) \Rightarrow S$
  2. Theorem (quantifier fun):$(\forall x.\exists y.\forall z.A(x,y,z)) \Rightarrow (\forall z.\forall x.\exists y.A(x,y,z))$
Assignment #12Peano arithmetic and Induction
  1. Theorem 7.3 (no number is it's own successor): $n\neq\sigma(n)$
  2. Theorem 7.4 (alternate definition of $\sigma$): $\sigma(n)=n+1$
  3. Theorem 7.5 (associativity of addition): $(m+n)+p=m+(n+p)$
  4. Theorem 7.6 (additive identity, part 2): $0+n=n$
  5. Theorem 7.7 (commutativity of adding $1$): $1+n=n+1$
  6. Theorem 7.8 (commutativity of addition):$m+n=n+m$
Assignment #13Peano arithmetic and Induction
  1. Theorem 7.11 (left multiplication by zero): $0\cdot m=0$
  2. Theorem 7.19 (nonzero naturals are positive):
    • (a) $0\leq n$
    • (b) $0\lt n \Leftrightarrow n\neq 0$
Assignment #14Sequences, Recursion, and Induction
  1. Theorem 8.3(a) (a useful identity): $n^2=n\cdot n$
  2. Theorem 8.3(b) (useful identity): $2\cdot n=n+n$
  3. Theorem 8.2(b) (power law): $z^m\cdot z^n=z^{m+n}$
  4. Theorem 8.2(c) (power law): $(z^m)^n=z^{m\cdot n}$
  5. Theorem 8.4 (quadratic beats linear):If $a+b\leq n$ then $a\cdot n+b\leq n^2$
Assignment #15Sequences, Recursion, and Induction
  1. Theorem 8.7 (Fib fun): $F_{n+3}+F_n=2\cdot F_{n+2}$
  2. Theorem 8.5(b) (basic sum property): $\displaystyle \sum_{i=0}^n s\cdot a_i = s\cdot \sum_{i=0}^n a_i$
  3. Theorem 8.11 (closed formula for binomial coefficients): $\displaystyle(m!\cdot n!)\cdot \binom{n+m}{m}=(n+m)!$
Assignment #16Real numbers and Field axioms
  1. Theorem 9.3 (cancellation for addition): If $x+z=y+z$ then $x=y$
  2. Theorem 9.2(b) (signed product): $(-1)\cdot(-1)=1$
  3. Theorem 9.2(c) (harder than it looks): $0\lt 1$
  4. Theorem 9.2(d) (not mod 2): $-1\neq 1$
Assignment #17Real numbers and Field axioms
  1. Theorem 9.4 (cancellation for multiplication): If $\neq 0$ and $z\cdot x=z\cdot y$ then $x=y$.
  2. Theorem 9.6 (multiplicative inverses are unique): If $z\cdot x=1$ and $z\cdot y=1$ then $x=y$.
  3. Theorem 9.10 (alternate additive inverse): $-x=-1\cdot x$
  4. Theorem 9.18 (adding inequalities):If $w\lt y$ and $x\lt z$ then $w+x\lt y+z$.
  5. Theorem 9.23 (scaling by a negative): If $z\lt 0$ and $x\lt y$ then $z\cdot y\lt z\cdot x$.
  6. Theorem (between): There exists a real number strictly between 0 and 1, i.e., $\exists r.0\lt r \text{ and }r\lt 1$.
Assignment #18Elementary Set Theory
  1. Theorem 10.5 (double negative): $\left(A'\right)'=A$
  2. Theorem 10.32 (always in the power set): $\{~~\}\in \mathscr{P}(A)$
  3. Theorem 10.34. (power sets of subsets): If $A\subseteq B$ then $\mathscr{P}(A)\subset\mathscr{P}(B)$.
  4. Theorem 10.38 (relative complement is not associative): If $x\in A$, $x\in B$, and $x\in C$ then $(A\setminus B)\setminus C\neq A\setminus (B\setminus C)$.
  5. Theorem 10.7 (a set of sets): $\{\,1,2\,\}\in\left\{\,Y:\{\,1\,\}\subseteq Y\right\}$
Assignment #19Elementary Set Theory
  1. Theorem 10.23(b) (∩ distributes over ∪):$ A \cap (B \cup C) \subseteq (A \cap B) \cup (A \cap C)$
  2. Theorem 10.37 (subsets are contagious):If $A \subseteq C$ and $B\subseteq D$ then $A\times B\subset C\times D$.
  3. Theorem 10.31 (not a subset):$A \nsubseteq B$ if and only if $\exists x.x \in A \cap B'$
  4. Theorem 10.27 (Baby DeMorgan):$A \setminus (B \cap C) = (A \setminus B) \cup (A \setminus C)$
  5. Theorem 10.29 (Papa DeMorgan): $\displaystyle\left(\bigcap_{i \in I} A_i\right)' = \bigcup_{j\in I} A_j'$
Assignment #20Functions and Composition
  1. Theorem 10.41 (composition is associative): If $h\colon A \to B$, $g\colon B \to C$, $f\colon C \to D$ then $$f\circ(g\circ h)=(f\circ g)\circ h.$$
  2. Theorem 10.53 (a) (identity maps are injective):The map $\mathrm{id}_A$ is injective.
  3. Theorem 10.53 (b) (identity maps are surjective):The map $\mathrm{id}_A$ is surjective.
  4. Theorem 10.46 (image of subsets):If $f\colon A \to B$, $S \subseteq T$, and $T \subseteq A$ then $f(S)\subseteq f(T)$.
Assignment #21Functions and Composition
  1. Theorem 10.43 (a linear bijection):If If $f\colon \mathbb{R} \to \mathbb{R}$ and $\forall x.f(x)=3\cdot x+1$ then $f$ is bijective.
  2. Theorem (inverse images respect intersection):If $f\colon A \to B$, $S \subseteq B$, $T \subseteq B$ then $$f^\mathrm{inv}(S \cap T)=f^\mathrm{inv}(S) \cap f^\mathrm{inv}(T)$$
  3. Theorem (inverse functions are bijective):If $f\colon A \to B$ and $f$ is bijective then $f^{-1}$ is bijective.
  4. Theorem 10.52 (inverse of a composition):If $f\colon A \to B$, $g\colon B \to C$, $f$ is bijective, and $g$ is bijective then $$(g \circ f)^{-1} = f^{-1} \circ g^{-1}$$
Assignment #22Equivalence relations and Partial orders
  1. Theorem (integer associates)Define $\sim$ to be the relation on $\mathbb{Z}$ such that for all $x,y\in \mathbb{Z}$, $$x\sim y\text{ if and only if }y=x\text{ or }y=−x$$ Then $\sim$ is an equivalence relation.
  2. Theorem ($\subseteq$ is a partial order)Let $A$ be a set and suppose $\sim$ is a relation on $\mathscr{P}(A)$ such that for all $S,T\in\mathscr{P}(A)$ $$S\sim T\text{ if and only if }S\subseteq T$$ Then $\sim$ is a partial order.
Assignment #23Equivalence relations and Partial orders
  1. Theorem 10.65Congruence mod $m$ is an equivalence relation on the set of integers.
  2. Theorem 10.66 (class representatives): Every integer $a$ is congruent mod $m$ to a unique natural number that is less than $m$, i.e., $\exists r.a \underset{m}{\equiv}r\text{ and }0\leq r\text{ and }r\lt m$ and if $a \underset{m}{\equiv} s$, $0\leq s$, and $s\lt m$ and $a \underset{m}{\equiv} t$, $0\leq t$, and $t\lt m$ then $s=t$.
Assignment #24Modular arithmetic
  1. Theorem 10.68 (modular addition):For any integers $a,b,c,d$, if $a \underset{m}{\equiv} b$ and $c \underset{m}{\equiv} d$ then $a+c \underset{m}{\equiv} b+d$
  2. Theorem 10.69 (modular multiplication):For any integers $a,b,c,d$, if $a \underset{m}{\equiv} b$ and $c \underset{m}{\equiv} d$ then $a\cdot c \underset{m}{\equiv} b\cdot d$

Lurch for Students

Lurch – This button will open a blank document with no rules or background material in the student version of Lurch. The only difference is that the student version does not have the Table or Instructor menus, and it will open in a restricted window useful for testing.

Lurch for Instructors

Lurch – This button will open a blank document with no rules or background material in the instructor version of Lurch.

Customize this Site

Instructors who would like to customize this site for use in their own courses can do that easily by forking this repository on GitHub.

  1. Sign into your account on Github (or create a free account).
  2. Go to github.com/kenmonks/lurch/fork and choose your account from the "Owner" dropdown. You can also optionally change the repository name. Then click "Create fork".
  3. Go to "https://github.com/your_account/your_sitename/settings/pages" where your_account is your GitHub account name and your_sitename is the name you chose for your site in the previous step.
  4. Tell it to deploy from a branch, and select the branch "main" with the default "/(root)" folder. Then click the "Save" button.
  5. After a minute or so you should be able to access your site at "https://your_account.github.io/your_sitename".

You can then replace the "index.html" file and other content with whatever you want to customize the site for use in your course. You will also be able to pull bug fixes and new features from my site in the future if you wish.