[FRIAM] TheoremDep

[Frank Wimberly]

Concatenate proofs.  This reminds me of the old joke:

An Engineer walks in her office and finds her trash can on fire.  She
gets the fire extinguisher and puts out the fire.

  The Mathematician walks in his office and finds his trash can on fire.
He gets the fire extinguisher and puts out the fire.

  The following day :

  The Engineer walks in her office and finds the trash can on fire on
top of her desk.  She gets the fire extinguisher and put out the fire.

  The Mathematician walks in his office and finds the trash can on fire
on top of his desk.  He takes the trash can and puts it on the floor.
He has reduced the problem to a previously solved state.  Too solve it
again would be redundant.


-----------------------------------
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 Wed, Mar 27, 2019, 2:50 PM glen∈ℂ <gepropella at gmail.com> wrote:

> It's not clear to me that the intent of that dependency project is to
> concatenate proofs.  Is that what you guys think it's purpose is?  It
> seems, to me, more like a reliability analysis, where the trustworthiness
> of any component depends (to a greater or lesser) extent on the
> trustworthiness of its parts ... weakest link of the (inferential) chain
> and all that.  I've seen the misapplication of various numerical solutions
> throughout my career.  And one of the important aspects of applying any
> given algorithm is the assurance that its inputs satisfy whatever
> requirements/assumptions are necessary for the output to be trustworthy.
> This seems similar.
>
> On 3/22/19 4:31 PM, Joe Spinden wrote:
> > 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
> >
> >
> > ============================================================
> > 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.471366.n2.nabble.com/FRIAM-COMIC>
> http://friam-comic.blogspot.com/ by Dr. Strangelove
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://redfish.com/pipermail/friam_redfish.com/attachments/20190327/2ae2a145/attachment.html>