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

Joe Shipman joeshipman at aol.com
Sat Jan 17 10:41:10 EST 2009

```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

```