Ken Monks
monks.scranton.edu
proveitmath.org

Proof Verification with Lurch Plus

Building the bridge to higher mathematics

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

Anonymous, 2024

Welcome to the home of Lurch — an open source math editor that can check your proofs!

Example Proof Gallery

Here are a few example proofs done in Lurch using the topics defined below.

Start Lurching!

Learning what a proof is can be the pursuit of a lifetime, but getting started with Lurch is easy!

Additional Information

Most users can get by with just the information provided above. For those of you who want to go deeper into the inner workings of Lurch, here are some useful links.

Start a New Document

Click one of the following buttons to open a new document in either the student version or instructor version of Lurch. The document will have no mathematical content or context whatsoever. You can start completely from scratch! If you prefer to start with some definitions or theorems available, try one of the blank documents with a context provided in the next section below.

Lurch for students

Lurch for Instructors

Example Definitions, Rules, and Theorems

Introduction to Mathematical Proof (Math 299), University of Scranton

Lurch allows instructors to completely customize Lurch by creating their own definitions, theorems, notes, textbook, and other course content.

Lurch was used successfully in my undergraduate bridge course for math majors, Math 299 at the University of Scranton, Spring 2024. These definitions and notes are very specific to my course, but are included here for instructors who want to use or modify them. Thus, these are not any sort of 'official' contexts or math content built into Lurch itself, but rather are just one example of specific content made by a specific instructor for a specific course. We hope to add additional mathematical content here from other instructors and courses in the future.

Cumulative Topics – each link 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 $\left(m,n\right)$, binomial coefficients $\binom{n}{k}$, 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 an expression 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. (view rules)
Sets, Equations, and Logic
Set Theory, Equations, Logic Theorems, Predicate Logic, Propositional Logic. This does not include Set Theory Theorems. (view rules)
Functions, Sets, Equations, and Logic
Functions, Set Theory Theorems, Set Theory, Equations, Logic Theorems, Predicate Logic, Propositional Logic. (view rules)
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 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. I am in the process of updating them. I also intend to revise the entire syllabus as a result 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 #06 Propositional 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 #07 Propositional 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 #08 Predicate 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 (De Morgan): $\neg (S\text{ and }T) \Rightarrow \neg S\text{ or } \neg T$
  6. Theorem (De Morgan): $\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 #09 Logic 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 #10 Logic 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 #11 Logic 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 #12 Peano arithmetic and Induction
  1. Theorem 7.3 (no number is its 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 #13 Peano 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 #14 Sequences, 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 #15 Sequences, 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 #16 Real 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 #17 Real numbers and Field axioms
  1. Theorem 9.4 (cancellation for multiplication): If $z\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 #18 Elementary 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)\subseteq\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 #19 Elementary 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 De Morgan): $A \setminus (B \cap C) = (A \setminus B) \cup (A \setminus C)$
  5. Theorem 10.29 (Papa De Morgan): $\displaystyle\left(\bigcap_{i \in I} A_i\right)' = \bigcup_{j\in I} A_j'$
Assignment #20 Functions 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 #21 Functions and Composition
  1. Theorem 10.43 (a linear bijection): 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 #22 Equivalence 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 #23 Equivalence relations and Partial Orders
  1. Theorem 10.65 Congruence 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 #24 Modular 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$

Final Exam!– try your hand at the Math 299 Final Exam from Spring 2024 (four parts)

Get Lurch!

Get Lurch! – If you’d like to use Lurch in your course or explore it on your own, you can access the materials directly from this site or customize a copy for your own needs. Detailed instructions on obtaining, customizing, and even installing Lurch locally on your computer are available here.