Re: TheoremDep

Posted by gepr on Mar 27, 2019; 9:11pm
URL: http://friam.383.s1.nabble.com/TheoremDep-tp7592833p7592839.html

Unfortunately, I have no sense of humor.  (Seriously.  I've been told so by many witty persons.)  So, the question remains.  Do you think that theorem dependency project is about concatenating proofs?

On 3/27/19 2:02 PM, Frank Wimberly wrote:

> 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.
>
>>> 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.

============================================================
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