[FOM] Proof assistants and conjectures

[Timothy Y. Chow]

On Wed, 14 Jan 2009, joeshipman at aol.com wrote:
> All mathematicians working in this area have a very robust sense of what 
> P != NP means and no?confusion about the equivalence of any 
> formalizations; but can anyone suggest some statement which is 
> significantly easier to formalize which is equivalent to P != NP ? (The 
> proof of equivalence can be as complicated as you like.)

Cellular automata might be marginally easier to formalize than Turing 
machines.

One can also appeal to descriptive complexity: for ordered structures,
P corresponds to first-order logic plus the least-fixed-point operator, 
while NP corresponds to second-order existential logic, but it's not clear 
that this is any simpler than formalizing a model of computation.

Tim