Skip to content

Commit

Permalink
Rebuild site with latest changes
Browse files Browse the repository at this point in the history
  • Loading branch information
@nathancarter
nathancarter committed Jul 23, 2024
1 parent fef61b0 commit 8f27d0e
Show file tree
Hide file tree
Showing 8 changed files with 49 additions and 120 deletions.
Binary file added site/img/proof-with-mistakes-screenshot.png
View file
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added site/img/topology-proof-screenshot.png
View file
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
113 changes: 21 additions & 92 deletions site/index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -92,7 +92,11 @@
<ul class="nav flex-column">
</ul>
</li>
<li class="nav-item" data-bs-level="2"><a href="#status" class="nav-link">Status</a>
<li class="nav-item" data-bs-level="2"><a href="#example-proof-in-lurch" class="nav-link">Example proof in Lurch</a>
<ul class="nav flex-column">
</ul>
</li>
<li class="nav-item" data-bs-level="2"><a href="#lurch-also-finds-mistakes" class="nav-link">Lurch also finds mistakes</a>
<ul class="nav flex-column">
</ul>
</li>
Expand Down Expand Up @@ -126,96 +130,21 @@ <h2 id="lurn-more">Lurn more</h2>
<p><a href="reference-toc/">References</a></p>
</div>
</div>
<h2 id="status">Status</h2>
<p>The latest version of Lurch is a web application that is in alpha testing at the
moment. <a href="http://lurchmath.github.io/lurchmath">You can try it online here!</a>
A simple example proof in propositional logic is shown below.</p>
<div class='lurch-embed' width='100%' height='500px' validate='true'>

<div class='header'>
We tell Lurch which symbols our mathematical system requires like this:
`Declare and, or, implies, not`.

<rule>
**Conjunction introduction:**
`If A` and `if B` then we can conclude `A and B`.
</rule>

<rule>
**Conjunction elimination:**
`If A and B` then we can conclude `A` and separately conclude `B`.
</rule>

<rule>
**Disjunction introduction:**
`If A` then we can conclude `A or B`, conclude `B or A`, or even both.
</rule>

<rule>
**Disjunction elimination:**

<subproof>
(Version 1) `If A or B` and `not A` then it must be `B`.
</subproof>
<subproof>
(Version 2) `If A or B` and `not B` then it must be `A`.
</subproof>
</rule>

<rule>
**Conditional introduction:**

To prove a conditional, we must construct a subproof of the following form.
<premise>
`Assume A`. Then, typically after some work, prove `B`.
</premise>
From that subproof, we can conclude `A implies B`.
</rule>

<rule>
**Conditional elimination:**

`If A implies B` and `if A`, then we can conclude `B`.
</rule>

<rule>
**Negation introduction:**

<premise>
If we start a subproof with "`assume A`" and we end it with a contradiction,
say `B` and `not B`, then we can end the subproof...
</premise>
...and conclude `not A`.
</rule>

<rule>
**Negation elimination:**

<premise>
If we start a subproof with "`assume not A`" and we end it with a contradiction,
say `B` and `not B`, then we can end the subproof...
</premise>
...and conclude `A`.
</rule>
</div>

<theorem>
**Contrapositive:** `If X implies Y` then `not Y implies not X`.
</theorem>
<proof>
`Assume X implies Y`. To establish the contrapositive, we must use a subproof.
<subproof>
`Assume not Y`. The easiest way to show $\neg X$ is with an inner subproof.
<subproof>
`Assume X`. Then we can apply the original assumption to conclude `Y`, but we
already know that `not Y` is true. That's a contradiction.
</subproof>
So outside that inner subproof, we can conclude `not X`.
</subproof>
Since we assumed $\neg Y$ and proved $\neg X$ from it, we can conclude
`not Y implies not X`.
</proof>
</div></div>
<h2 id="example-proof-in-lurch">Example proof in Lurch</h2>
<p>The green check marks show that Lurch has graded each step of this work correct.
Not shown in the picture are all the definitions of functions, sets, and
topological spaces preceding the theorem and proof.</p>
<p><img alt="Screenshot of a proof in point-set topology, graded by Lurch" src="img/topology-proof-screenshot.png" /></p>
<h2 id="lurch-also-finds-mistakes">Lurch also finds mistakes</h2>
<p>The following shows a proof with intentional mistakes added, to showcase Lurch's
ability to detect them. The yellow "?" and red "X" are part of Lurch's
feedback, while the red text hovering over the document has been added for the
purposes of explaining on this website why Lurch gave the marks it gave.</p>
<p><img alt="Screenshot of a proof containing two mistakes, graded by Lurch" src="img/proof-with-mistakes-screenshot.png" /></p>
<p>In the application, if the user hovers their mouse over the yellow "?" they will
get a message saying, "You have not yet convinced me of this." If they hover
their mouse over the red "X" they will get a message saying, "But you have
already used j."</p></div>
</div>
</div>

Expand Down Expand Up @@ -301,5 +230,5 @@ <h4 class="modal-title" id="keyboardModalLabel">Keyboard Shortcuts</h4>

<!--
MkDocs version : 1.6.0
Build Date UTC : 2024-07-22 21:55:20.502801+00:00
Build Date UTC : 2024-07-23 17:26:58.218268+00:00
-->
2 changes: 1 addition & 1 deletion site/search/search_index.json
View file

Large diffs are not rendered by default.

46 changes: 23 additions & 23 deletions site/sitemap.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,117 +2,117 @@
<urlset xmlns="http://www.sitemaps.org/schemas/sitemap/0.9">
<url>
<loc>https://lurchmath.github.io/</loc>
<lastmod>2024-07-22</lastmod>
<lastmod>2024-07-23</lastmod>
<changefreq>daily</changefreq>
</url>
<url>
<loc>https://lurchmath.github.io/about/</loc>
<lastmod>2024-07-22</lastmod>
<lastmod>2024-07-23</lastmod>
<changefreq>daily</changefreq>
</url>
<url>
<loc>https://lurchmath.github.io/how-to-create-a-lurch-site/</loc>
<lastmod>2024-07-22</lastmod>
<lastmod>2024-07-23</lastmod>
<changefreq>daily</changefreq>
</url>
<url>
<loc>https://lurchmath.github.io/how-to-toc/</loc>
<lastmod>2024-07-22</lastmod>
<lastmod>2024-07-23</lastmod>
<changefreq>daily</changefreq>
</url>
<url>
<loc>https://lurchmath.github.io/lurch-notation/</loc>
<lastmod>2024-07-22</lastmod>
<lastmod>2024-07-23</lastmod>
<changefreq>daily</changefreq>
</url>
<url>
<loc>https://lurchmath.github.io/lurch-sites-gallery/</loc>
<lastmod>2024-07-22</lastmod>
<lastmod>2024-07-23</lastmod>
<changefreq>daily</changefreq>
</url>
<url>
<loc>https://lurchmath.github.io/old-versions/</loc>
<lastmod>2024-07-22</lastmod>
<lastmod>2024-07-23</lastmod>
<changefreq>daily</changefreq>
</url>
<url>
<loc>https://lurchmath.github.io/reference-toc/</loc>
<lastmod>2024-07-22</lastmod>
<lastmod>2024-07-23</lastmod>
<changefreq>daily</changefreq>
</url>
<url>
<loc>https://lurchmath.github.io/tut-01-word-processor/</loc>
<lastmod>2024-07-22</lastmod>
<lastmod>2024-07-23</lastmod>
<changefreq>daily</changefreq>
</url>
<url>
<loc>https://lurchmath.github.io/tut-02-expository-math/</loc>
<lastmod>2024-07-22</lastmod>
<lastmod>2024-07-23</lastmod>
<changefreq>daily</changefreq>
</url>
<url>
<loc>https://lurchmath.github.io/tut-03-meaningful-math/</loc>
<lastmod>2024-07-22</lastmod>
<lastmod>2024-07-23</lastmod>
<changefreq>daily</changefreq>
</url>
<url>
<loc>https://lurchmath.github.io/tut-04-validation/</loc>
<lastmod>2024-07-22</lastmod>
<lastmod>2024-07-23</lastmod>
<changefreq>daily</changefreq>
</url>
<url>
<loc>https://lurchmath.github.io/tut-05-assumptions/</loc>
<lastmod>2024-07-22</lastmod>
<lastmod>2024-07-23</lastmod>
<changefreq>daily</changefreq>
</url>
<url>
<loc>https://lurchmath.github.io/tut-06-environments/</loc>
<lastmod>2024-07-22</lastmod>
<lastmod>2024-07-23</lastmod>
<changefreq>daily</changefreq>
</url>
<url>
<loc>https://lurchmath.github.io/tut-07-rules/</loc>
<lastmod>2024-07-22</lastmod>
<lastmod>2024-07-23</lastmod>
<changefreq>daily</changefreq>
</url>
<url>
<loc>https://lurchmath.github.io/tut-07b-metavariables/</loc>
<lastmod>2024-07-22</lastmod>
<lastmod>2024-07-23</lastmod>
<changefreq>daily</changefreq>
</url>
<url>
<loc>https://lurchmath.github.io/tut-08-document-header/</loc>
<lastmod>2024-07-22</lastmod>
<lastmod>2024-07-23</lastmod>
<changefreq>daily</changefreq>
</url>
<url>
<loc>https://lurchmath.github.io/tut-09a-real-math/</loc>
<lastmod>2024-07-22</lastmod>
<lastmod>2024-07-23</lastmod>
<changefreq>daily</changefreq>
</url>
<url>
<loc>https://lurchmath.github.io/tut-09b-real-math/</loc>
<lastmod>2024-07-22</lastmod>
<lastmod>2024-07-23</lastmod>
<changefreq>daily</changefreq>
</url>
<url>
<loc>https://lurchmath.github.io/tut-09c-real-math/</loc>
<lastmod>2024-07-22</lastmod>
<lastmod>2024-07-23</lastmod>
<changefreq>daily</changefreq>
</url>
<url>
<loc>https://lurchmath.github.io/tut-09d-real-math/</loc>
<lastmod>2024-07-22</lastmod>
<lastmod>2024-07-23</lastmod>
<changefreq>daily</changefreq>
</url>
<url>
<loc>https://lurchmath.github.io/tutorial-toc/</loc>
<lastmod>2024-07-22</lastmod>
<lastmod>2024-07-23</lastmod>
<changefreq>daily</changefreq>
</url>
<url>
<loc>https://lurchmath.github.io/what-is-a-lurch-site/</loc>
<lastmod>2024-07-22</lastmod>
<lastmod>2024-07-23</lastmod>
<changefreq>daily</changefreq>
</url>
</urlset>
Binary file modified site/sitemap.xml.gz
View file
Binary file not shown.
2 changes: 1 addition & 1 deletion site/tut-08-document-header/index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -113,7 +113,7 @@ <h1 id="hiding-and-showing-rules">Hiding and showing rules</h1>
"menuData" : {
"document" : {
"title" : "Document",
"items" : "editheader | validate clearvalidation | docsettings temptoggle"
"items" : "togglemeaning validate | docsettings"
}
}
}
Expand Down
6 changes: 3 additions & 3 deletions site/tut-09a-real-math/index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -114,14 +114,14 @@ <h1 id="real-mathematics-part-1">Real mathematics, part 1</h1>
</div>
<h2 id="okay-its-just-propositional-logic-but-theyre-real-proofs">Okay, it's just propositional logic, but they're real proofs</h2>
<p>One of the early topics in some introduction to proof courses is logic, often
starting with propositional logic. You may have noticed the example proof below
(in propositional logic) on <a href="../">the documentation home page</a>.</p>
starting with propositional logic. Consider the example propositional logic
proof below.</p>
<div class='lurch-embed' width='100%' height='500px' validate='true'>
{
"menuData" : {
"document" : {
"title" : "Document",
"items" : "editheader | validate clearvalidation | docsettings temptoggle"
"items" : "togglemeaning validate | docsettings"
}
}
}
Expand Down

0 comments on commit 8f27d0e

Please sign in to comment.