Is P=NP relevant to finding proofs of everyday mathematical propositions?

Question

Disclaimer: I don't know a whole lot about complexity theory beyond, say, a good undergrad class.

With increasing frequency I seem to be encountering claims by complexity theorists that, in the unlikely event that P=NP were proved and an algorithm with reasonable constants found, mathematicians wouldn't bother trying to prove things anymore beause we could just use our P-time algorithm to search for proofs. Usually this is part of an argument for why all mathematicians and logicians should care a lot about P=?=NP.

I think most of these claims are exaggerations of the first full paragraph on page 8 of the Cook's problem description for the Clay Institute (which itself is stated in a completely reasonable and unexaggerated manner).

However, it's quite clear from the Clay Institute description that P=NP is relevant only to classes of problems, parameterized by some integer $n$, for which we have already proved all three of the following:

1. the question is not independent of our chosen axioms ($T\vdash \phi\vee T\vdash \neg\phi$)
2. any proof of the proposition must have size at most polynomial in $n$
3. any proof of the negation of the proposition must have size at most polynomial in $n$

This way we know there's a proof of either the proposition or its negation, and the search problem for the one that does exist falls inside NP, so we can dovetail the two searches and stop when one of them succeeds.

This puzzles me. Most of the propositions mathematicians care about don't come in integer-parameterized classes, let alone classes with known proof-size bounds. Usually they come in classes of size 1 with no knowledge of proof-size. Is there some trick for turning the sorts of results mathematicians care about into these integer-parameterized-polynomially-bounded classes?

Example: how would you do this for the question of whether or not CH is independent of ZFC?

Cook and Reckhow's JSL article The Relative Efficiency of Propositional Proof Systems (which seems to be the starting point for the literature) actually mentions that if you take the problem class to consist of all propositions in some proof system (such as first-order predicate calculus), take the length of the proposition as the parameter, and take the question to be "is it entailed by the axioms", then at the time the paper was published (1979) no real-world proof system was known to have the desired property, and a few were known not to have the desired property.

I suppose I am being slightly lazy here, since the study of which problems have this property is a whole subfield with plenty of literature I could read, but really I'm only interested in whether or not that subfield's positive-results-to-date justify the claims I've been hearing lately. A reference to a paper containing the "trick" above would be fine as an answer.

Answer 1

Let me address the issue at the beginning of the original question: If P=NP were proved and an algorithm with reasonable constants found, would mathematicians stop trying to prove things? The relevant NP set in this situation seems to be the $L_1$ of Ryan Williams's answer, which I regard (or decode) as the set of pairs consisting of a proposition $P$ to be proved and an upper bound $n$, written in unary notation, for the proof length. If we had a polynomial time algorithm for this NP set, then I could apply it as follows. Take $P$ to be some proposition that I'm tempted to work on, and take $n$ to be larger than any proof that I'd have time to write out in my life. If the algorithm, applied to these inputs, says "no" then I shouldn't work on this problem, because any proof would be too long for me to write out. If the algorithm says "yes" then I still shouldn't work on the problem because a P-time algorithm for Ryan's $L_2$ could find the proof for me. All of this, however, depends on an extremely optimistic understanding of "reasonable constants". The $n$ I chose is (I hope) rather big, so even a quadratic-time algorithm (with a small coefficient on the quadratic term) could take a long time (longer than my lifetime).

The bottom line is that, if P=NP were proved with plausible constants in the running time, it would not be foolish for me to keep trying to prove theorems. (Even if it were foolish, I'd keep trying anyway, partly because it's fun and partly because people might like my proof better than the lexicographically first one.)

By the way, the system in which proofs are done should, for these purposes, not be simply an axiomatic system like ZFC with its traditional axioms and underlying logic. It should be a system that allows you to formally introduce definitions. In fact, it should closely approximate what mathematicians actually write. The reason is that, although I'm looking only for proofs short enough to write in my lifetime, that doesn't mean proofs short enough to write in primitive ZFC notation in my lifetime. I believe some (if not all) of the proofs I've published would, if written in primitive ZFC notation, be too long for a lifetime.

Answer 2

I myself think that proving that P=NP is neither necessary nor sufficient for getting computers to solve mathematics problems.

Not sufficient: it could produce long and virtually meaningless certificates of truth rather than proper proofs that we can actually understand and be interested in.

Not necessary: as mathematicians we do not solve the fully general problem, "Is there a proof of this statement that takes fewer than n symbols?" Rather, we focus on a very small subclass that consists of interesting and meaningful problems and we search for interesting and meaningful proofs. I myself believe that this problem is solvable in polynomial time (roughly speaking because I don't believe that humans have special abilities that computers will for ever lack).

Answer 3

Let me try a slightly more detailed answer than the previous ones. I don't know if it clears up your concerns, because I'm not completely sure what your concerns are. For any proof system, consider the languages

$L_1 = \{ P1^n ~|~n \in {\mathbb N}$ and Proposition $P$ has a proof in the system with at most $n$ symbols$\}$.

$L_2 = \{ P1^k ~|~n \in {\mathbb N}$ and Proposition $P$ has a proof in the system and the $k$-th bit of the lexicographically first proof of $P$ is 1$\}$.

If $P=NP$, then the two above languages can be solved in polynomial time (for "everyday" proof systems). This allows you to produce a proof of any fixed proposition $P$, when it exists, in time that is polynomial in the length of the shortest proof. We do not need to know the length of the shortest proof in advance. For example, if SAT is solvable in linear time (an open problem), then the below procedure should be implementable in no more than quadratic or cubic time in the length of the shortest proof.

I will outline why this is true. Suppose for explicitness that the running time for deciding both $L_1$ and $L_2$ is at most $c \cdot n$ where $n$ is the input length. First, run the program for $L_1$ on $P1$, $(\neg P)1$, $P1^2$, $(\neg P)1^2$, $P1^4$, $(\neg P)1^4$, $P1^8$, $(\neg P)1^8$, etc., until the program outputs "yes". The running time of this procedure is about $c(d+2)2^k$ where $d$ is the length of the proposition and $2^k$ is the smallest power of two that exceeds the length of the shortest proof. This determines an upper bound on the length of the shortest proof up to a multiplicative factor of two. (By performing a "binary search" in a similar way on the interval $[2^{k-1},2^k]$ with a slightly modified language, you could uncover the minimum length of a proof if you like, call it $p$. For us it suffices to have a good upper bound on the length.)

Suppose the program output "yes" on $P$ (rather than $\neg P$). Then run the program for $L_2$ on $P1^1$, $P1^2$, $\ldots$, $P1^p$ (or up to $P1^{2^k}$). Each call returns a bit of the lexicographically first proof of $P$ which has length $p$. The total running time is about quadratic in $p$ (with some extra constants $c$ and $d$).

If you're arguing that even this sort of running time must still be impractical for "everyday mathematical propositions", I would have to disagree. If the constant $c$ in the algorithms were provably gigantic (or more generally, the degrees of the polynomials in the running time) then this would be true, but we have very little knowledge of bounds on $c$ at this time.

Answer 4

It so happens that I asked an analogous question at CS Theory StackExchange. A brief informal summary is this. First, it is undecidable to determine if a given theorem is provable in ZFC, and this would not change if we knew P=NP. Second, for other mathematical theorems (I used Goldbach's conjecture), if P=NP, and if the theorem has a "short proof," then not only could we determine whether the theorem is true or false, we could also find a proof quickly. More precisely, a proof could be found "in time polynomial in the length of the statement and the length of the shortest proof" (to quote one respondent) using Levin's universal search algorithm.

Answer 5

The point is that, if P=NP, there would exist a universal algorithm (applicable not just to specific theorems) that would find proofs in time polynomial in length of the proof. Most important results have "small" proofs, at least in a suitably defined language, in the sense that checking the proof is certainly feasible. Hence the cost of finding the proof, i.e. deciding the theorem, is poly(feasible) = feasible.

This definitely is an optimistic reading, but the proof-finding algorithm is indeed parametrized, by the length of the proof.

Answer 6

The paper "A Personal View of Average-Case Complexity" by Russell Impagliazzo considers five different worlds depending on the average case complexity of NP-complete problems, one of them ("Algorithmica") having P=NP.

The different worlds are explained using the famous anecdote of Gauss and his teacher asking the class to add the numbers from 1 until 100, so it's a nice read for any mathematician. The focus of the article is on the consequences of the five different possibilities on the teacher being able to pose problems for which he knows the solution but which Gauss cannot solve. So it doesn't answer your question about "a trick to turn mathematics into NP-problems", but gives you an idea about the question in your title.

Answer 7

Others have already given good answers, but I'd like to point out that the constraint of "reasonable constants" is potentially much more stringent than most people think. For example, in the real world, space tends to be more expensive than time. So suppose that there is some proof of the Riemann hypothesis that is just barely small enough that we can just barely implement a computer program that, when run using all the world's computer resources, can just barely step through the entire proof and verify it within an acceptable human time-frame. Chances are, we would not have enough resources to write down such a proof explicitly; the computers would probably be constantly reusing space and erasing stuff that had been used in checking earlier stages of the proof but that would no longer be needed. The plan that Andreas Blass outlined, of writing down explicitly the length of the proof in unary and running our magic algorithm on this input, would not be feasible in this scenario.

Anyway, the point is that in today's world, one should not think of a proof as something that takes just a few million characters to write down explicitly. Although it is an important observation that it would be revolutionary to discover an algorithm for searching for proofs that is as efficient as verifying them, we should recognize that the claim that a proof of P = NP would achieve this is a slight exaggeration.

Answer 8

No, because if there is such a class, then your system does not have any formulas with variables.

.

"Is there some trick for turning the sorts of results mathematicians care about into"
the class-you-wanted-to-ask-about type?

Yes.

problem(2n) := "There is a proof of length n that the original statement is false."
problem(2n+1) := "There is a proof of length n that the original statement is true."