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ƃ ☣ <[email protected]> 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
