[FRIAM] TheoremDep

[Joe Spinden]

Of course not.  Not to mention that there are often several different 
proofs of any significant theorem.

Joe


On 3/22/19 3:54 PM, Frank Wimberly wrote:
> 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.
>
> -----------------------------------
> Frank Wimberly
>
> My memoir:
> https://www.amazon.com/author/frankwimberly
>
> My scientific publications:
> https://www.researchgate.net/profile/Frank_Wimberly2
>
> Phone (505) 670-9918
>
> On Fri, Mar 22, 2019, 12:18 PM uǝlƃ ☣ <gepropella at gmail.com 
> <mailto:gepropella at gmail.com>> wrote:
>
>
>     I saw this on reddit this morning and thought some of you might
>     like it:
>
>     https://sharmaeklavya2.github.io/theoremdep/
>     > Track dependencies between theorems.
>
>     > About TheoremDep
>     > 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.
>     >
>     > TheoremDep is generated using ConcepDAG. ConcepDAG is a tool to
>     visualize dependencies between things in the form of a static website.
>     >
>     > If you want to contribute, check out the source code of these
>     projects:
>     >
>     >     TheoremDep
>     >     ConcepDAG
>
>
>
>     -- 
>     ☣ uǝlƃ
>
>     ============================================================
>     FRIAM Applied Complexity Group listserv
>     Meets Fridays 9a-11:30 at cafe at St. John's College
>     to unsubscribe http://redfish.com/mailman/listinfo/friam_redfish.com
>     archives back to 2003: http://friam.471366.n2.nabble.com/
>     FRIAM-COMIC <http://friam.471366.n2.nabble.com/FRIAM-COMIC>
>     http://friam-comic.blogspot.com/ by Dr. Strangelove
>
>
> ============================================================
> FRIAM Applied Complexity Group listserv
> Meets Fridays 9a-11:30 at cafe at St. John's College
> to unsubscribe http://redfish.com/mailman/listinfo/friam_redfish.com
> archives back to 2003: http://friam.471366.n2.nabble.com/
> FRIAM-COMIC http://friam-comic.blogspot.com/ by Dr. Strangelove

-- 
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.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://redfish.com/pipermail/friam_redfish.com/attachments/20190322/c42d0247/attachment.html>