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
