[FRIAM] TheoremDep
glen∈ℂ
gepropella at gmail.com
Wed Mar 27 17:11:38 EDT 2019
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.
More information about the Friam
mailing list