[FOM] Proof Assistants and Conjectures (reply to Chow)

[joeshipman@aol.com]

I mean that I can't write it down in a formal language in less than a 
couple of pages. For RH on the other hand, I can do it in a few lines 
for some of the equivalent versions.


-----Original Message-----
From: Timothy Y. Chow <tchow at alum.mit.edu>
To: fom at cs.nyu.edu
Sent: Mon, 19 Jan 2009 9:01 am
Subject: Re: [FOM] Proof Assistants and Conjectures (reply to Chow)



Regarding the formalization of P = NP, Joe Shipman wrote:
>This is still unsatisfactorily complicated.

What criteria are you using here to judge whether the formalization is
"satisfactory"?  I can understand searching for a simple formalization 
as
a matter of curiosity or aesthetics.  But my original question was
motivated by utilitarian concerns.  A "complicated" formalization is 
not
necessarily unsatisfactory in this sense.  It would be unsatisfactory 
if
the formalization were so complicated that computers could not in 
practice
cope with it, or if it were difficult to use as a building block for 
other
theorems and conjectures.  But it doesn't seem that P = NP poses a 
problem
in this regard.  (Statements like "checkers is a draw," on the other 
hand,
might be a real pain from a practical standpoint---do you really want 
your
assistant to regenerate the proof each time it loads?  Alternatively, 
do
you really want to add it as an axiom?  But that is another topic.)

Tim
_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom