<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">https://www.amazon.com/author/frankwimberly</a><br><br>My scientific publications:<br><a href="https://www.researchgate.net/profile/Frank_Wimberly2">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">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">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">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">http://friam.471366.n2.nabble.com/<br>
FRIAM-COMIC</a> <a href="http://friam-comic.blogspot.com/" rel="noreferrer noreferrer" target="_blank">http://friam-comic.blogspot.com/</a> by Dr. Strangelove<br>
</blockquote></div>