I’ll comment with a story. Really, did you expect me to answer a
question with another question?
Andrew Gleason was one of my favorite professors, and the solver of (one
interpretation of) Hilbert’s 5th problem. At one time, I checked out
his proof. It was hopeless. The statement that he was proving was not at
all the same as Hilbert’s problem; rather it was the proof of the last
remaining unproved lemma in a proof outline somewhere.
The theorem dependency project has the potential of documenting, at
least, the trail that leads to the final proof. In many cases, the only
way to understand, even superficially, such a trail is to start at the
beginning. What I had tried was to get on the trail from the side.
--Barry
On 27 Mar 2019, at 17:11, glen∈ℂ wrote:
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
============================================================
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
