Ken Monks
monks.scranton.edu
proveitmath.org

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 an open source math editor that can check your proofs. 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

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 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 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 #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 (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 #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 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 #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 $\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)\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 #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 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 #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$

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.

Talk slides

Those of you who have attended my talks on Lurch can find my 'slides' from those talks here.

Get Lurch!

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

  1. Sign in to your account on Github (or create a free account).
  2. Return to this page and go to github.com/kenmonks/lurch/fork (you can just click that link) and choose your account from the "Owner" dropdown. You can also optionally change the repository name. Then click "Create fork".
  3. Go to here 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. Your students can click links on your site to open any Lurch files or other content you save in your repository.