<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p>Of course not. Not to mention that there are often several
different proofs of any significant theorem.</p>
<p>Joe</p>
<p><br>
</p>
<div class="moz-cite-prefix">On 3/22/19 3:54 PM, Frank Wimberly
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAA5dAfrv42QTm7_cTgjnU9JfWqPR0TUyRpqm=3wXwDu1kYSatA@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<div dir="auto">I can see that the proof of a theorem can be
constructed by concatenating proofs of theorems that it depends
on but I wonder if that would produce the most succinct and
comprehensible proof.<br>
<br>
<div data-smartmail="gmail_signature">-----------------------------------<br>
Frank Wimberly<br>
<br>
My memoir:<br>
<a href="https://www.amazon.com/author/frankwimberly"
moz-do-not-send="true">https://www.amazon.com/author/frankwimberly</a><br>
<br>
My scientific publications:<br>
<a href="https://www.researchgate.net/profile/Frank_Wimberly2"
moz-do-not-send="true">https://www.researchgate.net/profile/Frank_Wimberly2</a><br>
<br>
Phone (505) 670-9918</div>
</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Fri, Mar 22, 2019, 12:18 PM
uǝlƃ ☣ <<a href="mailto:gepropella@gmail.com"
moz-do-not-send="true">gepropella@gmail.com</a>> wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0 0 0
.8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
I saw this on reddit this morning and thought some of you
might like it:<br>
<br>
<a href="https://sharmaeklavya2.github.io/theoremdep/"
rel="noreferrer noreferrer" target="_blank"
moz-do-not-send="true">https://sharmaeklavya2.github.io/theoremdep/</a><br>
> Track dependencies between theorems.<br>
<br>
> About TheoremDep<br>
> TheoremDep contains many theorems and shows you the
dependencies for each theorem. Theorem X is said to be
dependent on theorem Y iff Y is used as a lemma in the proof
of X. Therefore, this website presents proofs in a way which
simultaneously achieves the goals of not assuming any prior
knowledge and making it easy to skip parts you already know.<br>
> <br>
> TheoremDep is generated using ConcepDAG. ConcepDAG is a
tool to visualize dependencies between things in the form of a
static website.<br>
> <br>
> If you want to contribute, check out the source code of
these projects:<br>
> <br>
> TheoremDep<br>
> ConcepDAG<br>
<br>
<br>
<br>
-- <br>
☣ uǝlƃ<br>
<br>
============================================================<br>
FRIAM Applied Complexity Group listserv<br>
Meets Fridays 9a-11:30 at cafe at St. John's College<br>
to unsubscribe <a
href="http://redfish.com/mailman/listinfo/friam_redfish.com"
rel="noreferrer noreferrer" target="_blank"
moz-do-not-send="true">http://redfish.com/mailman/listinfo/friam_redfish.com</a><br>
archives back to 2003: <a
href="http://friam.471366.n2.nabble.com/FRIAM-COMIC"
rel="noreferrer noreferrer" target="_blank"
moz-do-not-send="true">http://friam.471366.n2.nabble.com/<br>
FRIAM-COMIC</a> <a href="http://friam-comic.blogspot.com/"
rel="noreferrer noreferrer" target="_blank"
moz-do-not-send="true">http://friam-comic.blogspot.com/</a>
by Dr. Strangelove<br>
</blockquote>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">============================================================
FRIAM Applied Complexity Group listserv
Meets Fridays 9a-11:30 at cafe at St. John's College
to unsubscribe <a class="moz-txt-link-freetext" href="http://redfish.com/mailman/listinfo/friam_redfish.com">http://redfish.com/mailman/listinfo/friam_redfish.com</a>
archives back to 2003: <a class="moz-txt-link-freetext" href="http://friam.471366.n2.nabble.com/">http://friam.471366.n2.nabble.com/</a>
FRIAM-COMIC <a class="moz-txt-link-freetext" href="http://friam-comic.blogspot.com/">http://friam-comic.blogspot.com/</a> by Dr. Strangelove
</pre>
</blockquote>
<pre class="moz-signature" cols="72">--
Joe
Confidentiality Notice: This e-mail communication and any attachments may contain confidential and privileged information for the use of the designated recipients named above. If you are not the intended recipient, you are hereby notified that you have received this communication in error and that any review, disclosure, dissemination, distribution, or copying of it or its contents is prohibited. If you have received this communication in error, please notify me immediately by replying to this message and deleting it from your computer. Thank you.</pre>
</body>
</html>