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

[Timothy Y. 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