Re: TheoremDep

Posted by gepr on Mar 27, 2019; 8:50pm
URL: http://friam.383.s1.nabble.com/TheoremDep-tp7592833p7592837.html

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 [phone]
>>
>> On Fri, Mar 22, 2019, 12:18 PM uǝlƃ ☣ <[hidden email] <mailto:[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.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-comic.blogspot.com/ by Dr. Strangelove