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

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.

-
I saw Martin Davis talk last year and he said something along the lines of he wouldn't be at all surprised if P=NP, but only because people tend to forget how horrid a polynomial time algorithm can be. Even if we had a P-time algorithm to check for proofs, it might not be of any practical use. – Oliver Dec 2 '10 at 5:35
The gap accorded by people between polynomial and exponential time can be justified by the Moore's law. It guesses that computing capacities increase exponentially (this may have a limit due to some silicon proprieties, but uses of other technologies to continue this increase can be expected). If A problem is in P, even if it has a large exponent and constant, it will be easy one day to compute. – Lamine Dec 2 '10 at 9:59
Lamine: "If A problem is in P, even if it has a large exponent and constant, it will be easy one day to compute." Sorry, I disagree: there's no hope if the constant or exponent is of size $3!!!!!!!!!!!!!!!!!!!!!!!!$ (iterated factorials), for example! – Zen Harper Dec 3 '10 at 6:04
I meant that computing capacities increase faster than the complexity of any problem in P (if the Moore's law is true). That allows some hope to solve this problem one day. – Lamine Dec 3 '10 at 8:36
Very pedantic point: I think you mean $T \vdash \phi$ or $T \vdash \neg \phi$' under 1, not $T \vdash \phi \vee \neg \phi$', which is true for all $\phi$ (if we're using classical logic). – user7247 Jan 29 '11 at 18:39

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.

-
A very interesting observation: "people might like my proof better than the lexicographically first one" – Robin Kothari Dec 2 '10 at 19:10
Thank you, Andreas. Allow me to paraphrase the insight you've provided: nobody is trying to claim that anything will happen in time polynomial in the size of the proposition. The only claims being made are about things happening in time polynomial in the size of the shortest proof, if any. This side-steps the question of formal independence if we pretend that "no proof" means "shortest proof is infinitely long". This change-of-claim definitely leaves us with something which is objectively correct (although, I must say, subjectively less satisfying). – Adam Dec 2 '10 at 21:28
I should also add that it feels a bit peculiar: the proposition is the input to the process, and the convention is usually to measure asymptotic time in the size of the input rather than the size of the output. But the argument is still correct; it's just using an unusual metric. – Adam Dec 2 '10 at 21:28
@Adam: It's actually not so uncommon to have algorithms that run in time polynomial in the output rather than the input. For example, computing the permanent is #P hard, but it can be computed in time polynomial in its value. – Timothy Chow Dec 2 '10 at 22:51
@Adam: any algorithm which outputs a proof (if it exists) of a given proposition has running time bounded below by the length of the shortest proof—it needs time to write down the answer! And an algorithm which runs faster but does not output a proof would not be very satisfying to mathematicians; if a computer told me "the twin primes conjecture is true" without giving a proof, that wouldn't affect my life at all. – Tom Church Dec 3 '10 at 0:22

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.

-

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).

-
What's the point of a proof being interesting when humans no longer need to do any proving? We like interesting proofs because they teach us how to prove other things. – Andrew MacFie Mar 16 '15 at 1:38
@AndrewMacFie: Not just because interesting proofs teach us how to prove other things, but also because interesting proofs suggest to us other interesting questions that we might seek proofs for. Even in the most optimistic of P=NP scenarios, the issue of formulating interesting and useful questions would still be left to mathematicians. – Joshua Grochow Oct 28 '15 at 21:04

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.

-
Your algorithm will fail to terminate if I choose ZFC as my axioms and the Continuum Hypothesis as my proposition. – Adam Dec 2 '10 at 21:09
+1. Regarding the constants, it might be worth mentioning that Harvey Friedman has exhibited a proposition that is provable using ZFC + "for all $n$ there exists a strongly $n$-Mahlo cardinal" with at most $10^6$ symbols but that is not provable in ZFC alone using less than $10^{1000}$ symbols (in both cases allowing abbreviations). cs.nyu.edu/pipermail/fom/2006-February/010056.html Though Friedman's proposition does not directly address Adam's question as posed, it does illustrate the subtleties of bounding the actual sizes of actual proofs (as opposed to their asymptotic growth). – Timothy Chow Dec 2 '10 at 21:19
@Adam, of course, you'd need to use a proof system rich enough to express the proof of the independence of the Continuum Hypothesis from ZFC. But I'm not sure what your point is. One can find many other examples of theorems you can't prove within a given proof system; how does that show P=NP is irrelevant to finding proofs of everyday math propositions? – Ryan Williams Dec 3 '10 at 2:48
@RyanWilliams ZFC is rich enough to express the proof of the independence of the Continuum Hypothesis from ZFC. But you have to encode the statement (of independence) in the language of ZFC (as a single proposition). So I agree with Adam that it is a fault of your algorithm, not a fault of ZFC. – Thomas Klimpel Oct 21 '15 at 11:34

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.

-

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.

-
David, the algorithm would only work if a polynomial-sized proof existed. If one didn't, the algorithm would simply fail to terminate, but you'd never know the difference between "will never terminate" and "needs to run just a bit longer". So the algorithm would be useless without prior knowledge of the proof size. It still appears that the ramifications are being over-hyped. – Adam Dec 2 '10 at 2:51
Ricky, your algorithm will not always halt. Choose your axioms to be ZFC and your proposition to be the Continuum Hypothesis. Your algorithm will run forever since there is no proof of either CH or $\neg$CH from ZFC, let alone one which is polynomial in the length of CH! Regarding your other question: if the size $|p|$ of a proof $p$ is polynomial in $n$, then $|p|\leq\underset{0\leq i<k}\sum a_i\cdot n^{b_i}$; the $a_i$ are the coefficients and the $b_i$ are the exponents (I should have written "coefficients and exponents as inputs"). – Adam Dec 2 '10 at 4:08
"Choose your axioms to be ZFC and your proposition to be the Continuum Hypothesis" and my proof size as ... ? Once it checks all potential proofs of the given size, it will halt on "no short proof" (if ZF is consistent). – Ricky Demer Dec 2 '10 at 5:24
Adam, the vast majority of proofs found by humans are short. There's the occasional gigantic 100-page proof, but if the vast majority of proofs could be generated by machine, then the impact on mathematical practice would be large. – arsmath Dec 2 '10 at 14:51
"and my proof size is..." not listed as an input to your algorithm. – Adam Dec 2 '10 at 22:08

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"

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."

-
Ricky, is there any chance you could point me to a paper on the "No, because" part? Also, I think you may have misunderstood the requested "trick" -- the algorithm you present works only if we already know that the problem satisfies conditions (1)+(2)+(3). By "trick" I meant a method of converting arbitrary problems of general mathematical interest into problems which satisfy (1)+(2)+(3) -- or else a proof that no such thing can exist (which seems to be what the first part of your answer is saying, although I would appreciate further clarification). Thank you! – Adam Dec 1 '10 at 23:10
No, because :-) it's too simple for there to be a paper on it. Take a logical axiom, substitute a formula with at least one variable in it for each of the atoms, then keep using substitution to change the variables involved. Do this arbitrarily many times, then do what would be done in an ordinary proof of the problem instance or it's negation. This shows that for all n, if the problem instance is decidable, then there are arbitrarily long proofs, so in particular the proof lengths will not be bounded above by a polynomial in n. (continued below) – Ricky Demer Dec 1 '10 at 23:25
(continued from above) For all original problems, {problem(n) : n in N} is a family of problems which are finitistically checkable, such that (if are system can work with tuples, then) each true instance has a proof whose length is bounded by a polynomial in n, and (if our system is consistent, then) no false instance has such a proof. These hold independently of anything the original problem may or may not satisfy. – Ricky Demer Dec 2 '10 at 1:34

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.

-
Thanks Joseph, but my question is different -- you write "restrict attention to polynomially-long proofs", whereas I am questioning the practicality of that assumption. I actually considered posting to the complexity theory stackexchange, but ultimately the subjective part ("the propositions mathematicians care about") is the most delicate part, which is why I asked mathematicians instead of complexity theorists. – Adam Dec 1 '10 at 22:56
If you're ignoring the input size, why bother using an algorithm whose one and only virtue is its running time as a function of the input size? If we assume that proofs bigger than $10^{12}$ don't matter, then brute-force search is also constant-time, so it is asymptotically just as good as any other algorithm. Worse, if your algorithm has a constant which is $2^{2^{2^{10^{12}}}}$ iit is actually worse than brute-force search not only in asymptotic terms but absolute terms as well! These are the perils of using asymptotic analysis in a situation where everything is constant – Adam Dec 2 '10 at 6:05