[FRIAM] TheoremDep

[Barry MacKichan]

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