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ƃ ☣ <geprope...@gmail.com
<mailto:geprope...@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.
============================================================
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
