forked from lurchmath/minimal-lurch-site
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.html
232 lines (192 loc) · 14.7 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
<!--<!DOCTYPE html>-->
<html lang="en">
<head>
<meta charset="utf-8">
<title>Ken Monks | Professor of Mathematics</title>
<meta name="description" content="This is the website of Dr. Kenneth G. Monks, Professor of Mathematics at the University of Scranton.">
<meta name="keywords" content="math academy, summer courses, math proof camp, math proofs, mathematical proof, proof class, proof course, summer math camp, summer math program, summer math class, math camp, math program, math class, MATHCOUNTS, AMC, AIME, USAMO, IMO, ARML, math contest training, math competition training, math olympiad, AP olympiad, Intel Science, ISEF, ISTS, Regeneron competition, Siemens competition, math gifted, summer school program, camps for kids, academic summer camp, summer academy, summer schools, summer school usa, summer academic programs, summer classes, academy of mathematics, university of scranton, Lurch, Lehigh Valley ARML">
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<link rel="stylesheet" href="https://monks.scranton.edu/wp-content/themes/Monks/bootstrap/css/bootstrap.min.css">
<link rel="stylesheet" href="https://monks.scranton.edu/wp-content/themes/Monks/bootstrap/css/bootstrap-theme.min.css">
<link rel="stylesheet" href="//maxcdn.bootstrapcdn.com/font-awesome/4.1.0/css/font-awesome.min.css">
<link rel="stylesheet" href="https://monks.scranton.edu/wp-content/themes/Monks/social-buttons-3.css">
<link rel="stylesheet" href="https://monks.scranton.edu/wp-content/themes/Monks/style.css" >
<link href='//fonts.googleapis.com/css?family=Open+Sans:400,600,400italic,700,300' rel='stylesheet' type='text/css'>
<script src="//ajax.googleapis.com/ajax/libs/jquery/1.11.1/jquery.min.js"></script>
<script src="//maxcdn.bootstrapcdn.com/bootstrap/3.2.0/js/bootstrap.js"></script>
<script>
window.MathJax = {
tex: {
inlineMath: [ ['$','$'], ["\\(","\\)"] ],
processEscapes: true
}
};
</script>
<script src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-svg.js" id="MathJax-script"></script>
</head>
<body>
<div id="wrap">
<div id="header-block">
<nav class="navbar" role="navigation">
<div class="container">
<div class="navbar-header">
<a class="navbar-brand" href="/"><div id="top-logo">
<h2>KEN MONKS</h2>
<h3><span style="font-size:1.1em;position:relative;top:-1px">∎</span> Professor of Mathematics <span style="font-size:1.1em;position:relative;top:-1px">∎</span></h3>
<h4>[email protected]</h4>
</div></a>
</div>
</nav>
</div>
<div id="content-block">
<div class='container'>
<script>
const openLurch = (url) => {
const height = 0.85 * window.screen.height
const width = 853
const top = 0.075 * window.screen.height
const left = (window.screen.width - width)/2
var features = 'width=853, height='+height+', top='+top+', left='+left+
', toolbar=no, menubar=no, location=no, status=no'+
', noopener, noreferrer'
window.open(url, '_blank', features)
}
</script>
<style>
dd {
margin-bottom:0.5rem;
margin-left:1rem;
}
#content-block code {
background: #e7f3fd;
font-size: 110%;
}
</style>
<div style='display: flex; align-items: center; justify-content: space-between;padding-bottom:2rem;'>
<h1 style='margin:0;'>Lurch for Math 299</h1>
<img src='lurchlogo.png' style='margin-left:10px' width='15%'>
</div>
<p>Lurch is a math editor that can check your proofs (coauthored with Nathan Carter). Instructors who would like to create their own Lurch course materials using the rule libraries and content from my <a href='https://monks.scranton.edu/math299'>Math 299 course (Spring 2024)</a> can find supporting materials here. NOTE: much of this is under construction.</p>
<h2>Lurch for Instructors</h2>
<a href='' class='button' onclick="openLurch('app/?config=minimal-instructor'); return false;">
Lurch</a> – is a math word processor that can check your proofs! This button will open a blank document with no rules or background material in the instructor version of Lurch.
<h2>Math 299 Lurch Rule Libraries</h2>
<div style=
'background-color:#e7f3fd;
padding:1rem 1rem 0.25rem 1rem;
margin-left:0;
border-radius: 12pt;'>
<p><strong><span style='font-size:110%'>Cumulative Topics</span></strong> – each link one opens a blank Lurch document whose context consists of the rules for that topic, and those from the topics above it.</p>
<dl>
<dt><a href="app/?config=minimal-instructor&load=../math/Prop.lurch">Propositional Logic</a></dt>
<dd>defines <code>and</code>, <code>or</code>, <code>not</code>, <code>implies</code>, <code>iff</code>, and <code>contradiction</code> (<a href='app/?config=minimal-instructor&load=../math/Prop-Rules.lurch'>view rules</a>)</dd>
<dt><a href="app/?config=minimal-instructor&load=../math/Pred.lurch">Predicate Logic with Equality</a></dt>
<dd>defines <code>forall</code> $\left(\forall\right)$, <code>exists</code> $\left(\exists\right)$, <code>equality</code> $\left(=\right)$, <code>unique existence</code> $\left(\exists!\right)$ (<a href='app/?config=minimal-instructor&load=../math/Pred-Rules.lurch'>view rules</a>)</dd>
<dt><a href="app/?config=minimal-instructor&load=../math/Logic-theorems.lurch">Logic Theorems</a></dt>
<dd>provides some common theorems from Logic (<a href="app/?config=minimal-instructor&load=../math/Logic-theorems-Rules.lurch">view rules</a>)</dd>
<dt><a href="app/?config=minimal-instructor&load=../math/Peano.lurch">Natural Numbers</a></dt>
<dd>the Peano Axioms for the Natural Numbers (<a href="app/?config=minimal-instructor&load=../math/Peano-Rules.lurch">view rules</a>)</dd>
<dt><a href="app/?config=minimal-instructor&load=../math/Number-theory.lurch">Number Theory Definitions</a></dt>
<dd>defines, <code>less than</code> $\left(\lt\right)$, <code>divides</code> $\left(\mid\right)$, <code>prime</code>, <code>even</code>, <code>odd</code> (<a href="app/?config=minimal-instructor&load=../math/Number-theory-Rules.lurch">view rules</a>)</dd>
<dt><a href="app/?config=minimal-instructor&load=../math/Equations.lurch">Equations</a></dt>
<dd>defines a single ‘rule’ that enables Lurch to validate transitive chains of equalities without needing substitution, reflexivity, symmetry, or transitivity (<a href="app/?config=minimal-instructor&load=../math/Equations-Rules.lurch">view rules</a>)</dd>
<dt><a href="app/?config=minimal-instructor&load=../math/Number-theory-theorems.lurch">Number Theory Theorems</a></dt> <dd>provides some useful theorems from Number Theory that are provable from the Peano Axioms (<a href="app/?config=minimal-instructor&load=../math/Number-theory-theorems.lurch">view rules</a>)</dd>
<dt><a href="app/?config=minimal-instructor&load=../math/Sequences.lurch">Sequences and Recursion</a></dt>
<dd>defines <code>summation</code> $\left(\sum\right)$, <code>Fibonnaci numbers</code> $\left(F_n\right)$, <code>factorial</code> $\left(!\right)$, <code>multinomial coefficients</code> $\binom{n}{k}$, <code>binomial coefficients</code>, <code>exponentiation</code> $\left(z^n\right)$ (<a href="app/?config=minimal-instructor&load=../math/Sequences-Rules.lurch">view rules</a>)</dd>
<dt><a href="app/?config=minimal-instructor&load=../math/Reals.lurch">Real Numbers</a></dt>
<dd>defines the field axioms for the Real Numbers (<a href="app/?config=minimal-instructor&load=../math/Reals-Rules.lurch">view rules</a>)</dd>
<dt><a href="app/?config=minimal-instructor&load=../math/Sets.lurch">Set Theory</a></dt>
<dd>defines <code>in</code> $\left(\in\right)$, <code>subset</code> $\left(\subseteq\right)$, <code>intersection</code> $\left(\cap\right)$, <code>union</code> $\left(\cup\right)$, <code>complement</code> $\left(‘\right)$, <code>set difference</code> $\left(\setminus\right)$, <code>powerset</code> $\left(\mathscr{P}\right)$, <code>Cartesian product</code> $\left(\times\right)$, <code>finite set</code> $\left(\{ \ldots \}\right)$, <code>tuple</code> $\langle\ldots\rangle$, <code>Indexed Union</code> $\left(\bigcup\right)$, <code>Indexed Intersection</code> $\left(\bigcap\right)$, <code>Set Builder notation</code> $\left(\{ z : \ldots\}\right)$ (<a href="app/?config=minimal-instructor&load=../math/Sets-Rules.lurch">view rules</a>)</dd>
<dt><a href="app/?config=minimal-instructor&load=../math/Functions.lurch">Functions</a></dt>
<dd>defines <code>maps</code> $\left(f\colon A \to B\right)$, <code>function application</code> $\left(f(x)\right)$, <code>maps to</code> $\left(\mapsto\right)$, <code>image</code> $\left(f(U)\right)$, <code>identity map</code> $\left(\text{id}_A\right)$ <code>inverse image</code> $\left(f^\text{inv}(U)\right)$, <code>composition</code> $\left(\circ\right)$, <code>inverse function</code> $\left(f^{-1}\right)$, <code>injective</code>, <code>surjective</code>, <code>bijective</code> (<a href="app/?config=minimal-instructor&load=../math/Functions-Rules.lurch">view rules</a>)</dd>
<dt><a href="app/?config=minimal-instructor&load=../math/Relations.lurch">Relations</a></dt>
<dd>defines <code>reflexive</code>, <code>symmetric</code>, <code>transitive</code>, <code>irreflexive</code>, <code>antisymmetric</code>, <code>total</code>, <code>partial order</code>, <code>strict partial order</code>, <code>total order</code>, <code>equivalence relation</code>, <code>partition</code>, <code>equivalence class</code> $[a]$ (<a href="app/?config=minimal-instructor&load=../math/Relations-Rules.lurch">view rules</a>)</dd>
</dl>
</div>
<h2>Other Useful Contexts</h2>
<div style=
'background-color:#e7f3fd;
padding:1rem 1rem 0.25rem 1rem;
margin-left:0;
border-radius: 12pt;'>
<dl>
<dt><a href='app/?config=minimal-instructor&load=../math/Equations-Logic.lurch'>Equations and Logic Only</a> </dt>
<dd> Equations, Logic Theorems, Predicate Logic, Propositional Logic.</dd>
<dt><a href='app/?config=minimal-instructor&load=../math/Sets-Equations-Logic.lurch'>Sets, Equations, and Logic</a></dt>
<dd> Set Theory, Equations, Logic Theorems, Predicate Logic, Propositional Logic.</dd>
<dt><a href='app/?config=minimal-instructor&load=../math/Functions-Sets-Equations-Logic.lurch'>Functions, Sets, Equations, and Logic</a></dt>
<dd>Functions, Set Theory, Equations, Logic Theorems, Predicate Logic, Propositional Logic.</dd>
</dl>
</div>
<h2>Documentation</h2>
<ul class='disc'>
<li><a href='app/?config=minimal-instructor&load=../help/quick-start-guide.lurch'>Quick Start Guide</a></li>
<li><a href='app/?config=minimal-instructor&load=../help/example-proofs.lurch'>Examples</a> – a few proofs done in Lurch using the topics defined above.</li>
<li><a href="https://lurchmath.github.io/lurch/parsers/lurch-parser-docs.html">Lurch
Syntax</a> – a quick reference showing how to type various math expressions in Lurch</li>
</ul>
<h2>Example Assignments</h2>
<div>
<p><strong><span style='font-size:110%'>Math 299 Spring 2024 Assignments</span></strong> – 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. But we hope to update them soon.</p>
<dl>
<dt><a href="app/?config=minimal-instructor&load=../assignments/assignment-12.lurch">Assignment #12</a></dt>
<dd>Peano arithmetic and induction.</dd>
<dt><a href="app/?config=minimal-instructor&load=../assignments/assignment-13.lurch">Assignment #13</a></dt>
<dd>Peano arithmetic and induction.</dd>
<dt><a href="app/?config=minimal-instructor&load=../assignments/assignment-14.lurch">Assignment #14</a></dt>
<dd>Sequences, Recursion, and Induction.</dd>
<dt><a href="app/?config=minimal-instructor&load=../assignments/assignment-15.lurch">Assignment #15</a></dt>
<dd>Sequences, Recursion, and Induction.</dd>
<dt><a href="app/?config=minimal-instructor&load=../assignments/assignment-16.lurch">Assignment #16</a></dt>
<dd>Real numbers and field axioms.</dd>
<dt><a href="app/?config=minimal-instructor&load=../assignments/assignment-17.lurch">Assignment #17</a></dt>
<dd>Real numbers and field axioms.</dd>
<dt><a href="app/?config=minimal-instructor&load=../assignments/assignment-18.lurch">Assignment #18</a></dt>
<dd>Elementary Set Theory.</dd>
<dt><a href="app/?config=minimal-instructor&load=../assignments/assignment-19.lurch">Assignment #19</a></dt>
<dd>Elementary Set Theory.</dd>
<dt><a href="app/?config=minimal-instructor&load=../assignments/assignment-20.lurch">Assignment #20</a></dt>
<dd>Functions and composition.</dd>
<dt><a href="app/?config=minimal-instructor&load=../assignments/assignment-21.lurch">Assignment #21</a></dt>
<dd>Functions and composition.</dd>
<dt><a href="app/?config=minimal-instructor&load=../assignments/assignment-22.lurch">Assignment #22</a></dt>
<dd>Equivalence relations and partial orders.</dd>
<dt><a href="app/?config=minimal-instructor&load=../assignments/assignment-23.lurch">Assignment #23</a></dt>
<dd>Equivalence relations and congruence.</dd>
<dt><a href="app/?config=minimal-instructor&load=../assignments/assignment-24.lurch">Assignment #24</a></dt>
<dd>Modular arithmetic.</dd>
</dl>
</div>
<h2>Lurch for Students</h2>
<a href='' class='button' onclick="openLurch('app/'); return false;">
Lurch</a> – 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 Instructor menu.
</div><!-- container -->
</div><!-- content-block -->
</div><!-- wrap -->
<footer>
<div id="footer-block">
<div class="container">
<div class="row">
<div class="col-xs-12">
<h3><a href="http://monks.scranton.edu/">Dr. Kenneth G. Monks</a></h3>
Department of Mathematics<br />
University of Scranton<br />
Scranton, PA 18510
</div>
</div>
<div class="row" id="more-contact-info">
<div class="col-xs-12 col-md-6" id="email-footer">
<span class="glyphicon glyphicon-envelope"></span> <a href="mailto:[email protected]">[email protected]</a><br />
</div>
<div class="col-xs-12 col-md-6" id="facebook-footer">
<span class="fa fa-superscript"></span> <a href="https://proveitmath.org">Prove it! Math Academy</a>
</div>
</div><!-- row -->
</div>
<div id="copyright">
Copyright © Kenneth G. Monks | <a href="/acknowledgments">Acknowledgments</a>
</div>
</div>
</footer>
</body>
</html>