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.
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.
and
, or
, not
,
implies
, iff
, and
contradiction
(view rules)
forall
$\left(\forall\right)$,
exists
$\left(\exists\right)$,
equality
$\left(=\right)$,
unique existence
$\left(\exists!\right)$ (view rules)
less than
$\left(\lt\right)$,
divides
$\left(\mid\right)$, prime
,
even
, odd
(view rules)
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)
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)
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)
reflexive
, symmetric
,
transitive
, irreflexive
,
antisymmetric
, total
,
partial order
, strict partial order
,
total order
, equivalence relation
,
partition
, equivalence class
$[a]$
(view rules)
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.
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)
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)
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)
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.
topological space
, open
,
closed
, and continuous
(in a
toplogical space). Includes the Functions library above. (view rules)
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.
Instructors who would like to customize this site for use in their own courses can do that easily by forking this repository on GitHub.
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.