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.
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 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.
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.
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 – This button will open a blank document with no rules or background material in the instructor version of Lurch.
Those of you who have attended my talks on Lurch can find my 'slides' from those talks here.
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.
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.
main
with the default
/(root)
folder. Then click the "Save" button.
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.