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

joeshipman@aol.com joeshipman at aol.com
Mon Jan 19 16:30:51 EST 2009

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 
a matter of curiosity or aesthetics.  But my original question was
motivated by utilitarian concerns.  A "complicated" formalization is 
necessarily unsatisfactory in this sense.  It would be unsatisfactory 
the formalization were so complicated that computers could not in 
cope with it, or if it were difficult to use as a building block for 
theorems and conjectures.  But it doesn't seem that P = NP poses a 
in this regard.  (Statements like "checkers is a draw," on the other 
might be a real pain from a practical standpoint---do you really want 
assistant to regenerate the proof each time it loads?  Alternatively, 
you really want to add it as an axiom?  But that is another topic.)

FOM mailing list
FOM at cs.nyu.edu

More information about the FOM mailing list