[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
More information about the FOM
mailing list