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

[Joe Shipman]

P != NP is not so easy to formalize because of the background 
necessary to define a model of computation and the complexity classes 
P and NP. 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.)

For the Riemann Hypothesis, the simplest equivalent formulation I 
know is Lagarias's: Let H(n) = 1 + 1/2 + ... + 1/n, RH is equivalent to

"For all n, the sum of the divisors of n is <= H(n) + ln(H(n))*exp(H(n))."

This has only one quantifier but of course it involves real numbers 
and real functions. There are arithmetical equivalents which are not 
too hard which involve 3 quantifiers (formalizing that the Mobius 
function is eventually dominated by x^alpha whenever alpha > 1/2 ) 
but I'd like to know if there is an arithmetical equivalent that is 
easy and requires only one quantifier.

-- Joe Shipman