Of course not. Not to mention that there are often several different proofs of any significant theorem.
Joe
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ƃ ☣ <[hidden email]> 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-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.
| Free forum by Nabble | Edit this page |