Is This a Proof?
Seeking the limits of mathematical proofs
Ivan Vinogradov was a famous mathematician who created a whole method, named after him, that allowed him to make major advances on many open number theoretic problems. These included his theorem on the Weak Goldbach Conjecture and many others.
Today Ken and I wish to talk about a new type of “mathematical proof,” illustrating it for the Weak Goldbach Conjecture.
It is strange, pushes the limits of what we usually call a proof, but still might be considered a proof. Our plan is to present it first abstractly, then give a concrete example of the new style “proof.” The central questions today are: Is this new type of proof really a proof, and is it new?
What Is A Proof?
We know what a mathematical proof is. It is a convincing argument that some mathematical statement is correct. The rigor of proofs has changed slowly over the years, yet today we would all agree what constitutes a proof and what does not. Of course some are short and straightforward, some are short and complex, some are long and complex, few are long and straightforward.
The acid test is: can a proof be checked? If it cannot then most would argue it is not a proof. A poorly written proof may fail this test, even if the writer of the proof is convinced of its correctness. Some proofs over the years have been rejected because they failed this checking test, and some that failed were later judged to be correct. Many “correct” proofs still have typos or minor errors that are easy for a checker to fix. A typo of for may be easy to spot, and thus a proof that is technically incorrect is really fine.
Computer Proofs
Let be some statement we wish to prove. A standard proof would be a written argument that convinces you and others that is true. If the proof uses computation then what usually happens is:
- For some statement you prove that .
- Then you use your computer to check that is correct.
This of course then shows that is proved. Well, this is the issue with computer-based proofs. The fear is that the checking of may be faulty due to a program error or even a hardware error. This can be reduced by having people review the programs, or even better having them independently write their own programs to check . But there remains some feeling—for many—that such proofs could be wrong. We now have many proofs that no human can check, including proofs of the Four-Color Theorem (until recently) and this year’s advance on Paul Erdős’s Discrepancy problem (EDP). Many are uncomfortable with proofs of this kind, proofs that rely on massive computation. In any case we will consider human proofs and machine proofs as “standard” types of proofs. For thoughtful comments on machine proofs see this by Robert Pollack.
We think we have discovered a new type of proof—it fits into neither of these categories.
Monte Carlo Proofs
We will now describe our new type of proof. It is a type of computer-based proof, but one that ups the ante and is even more problematic. We still think it is quite interesting and should be studied.
So let look at a new way to prove . Let and be additional statements for . The keys are the following:
- We can prove that for each that .
- We can also prove that is true for at least of the indices .
- The statement is easy to check for any index by computation.
Then we can proceed as follows. Pick a set of random indices. For each in this set, check that is true. We claim that if all check correctly, then the probability that is true is at least .
The point is that each time we select an index there is a probability at least that is true. Since we check that is true, follows. But we may have selected an index so that is not true. The chance that this happens times is clearly at most , and so we have the claimed probability.
An Example
We return to the Weak Goldbach Conjecture. Vinogradov, in the 1930’s, famously proved that every sufficiently large odd number is the sum of at most three primes. His “sufficiently large” was not effective at first: he proved there was a constant so that all odd numbers larger than it were the sums of three primes. In 1956 it was shown that was upper-bounded by —a pretty large number. This was reduced in 2002 by Liu Ming-Chit and Wang Tian-Ze to approximately —still pretty large. Computer searches still cannot even get near such a bound.
The long-term goal of course has been to reduce this constant and prove eventually the following theorem:
Theorem 1 Every odd integer greater than can be expressed as the sum of three primes.
Recently this has been achieved by Harald Helfgott, who technically proved that the theorem is true for all odd numbers greater than . Computer searches had already verified the theorem up to . But let us cycle back to the situation before last year where was still on the order of . Let be the statement that all odd numbers below are the sum of at most three odd primes. The set of prime numbers below has density order-of . The key concept is:
Definition 2 A subset of the even numbers below is complementary to if every odd number below can be written as where and .
By a probabilistic argument, most subsets of size are complementary, where is a small known constant. (Indeed some finer results are now known.) The size is not too large, and the numbers themselves have only order- size. The final ingredient comes from the known heuristic bounds on Goldbachs’ Conjecture itself. For most even numbers , one is highly likely to find primes and summing to within trials.
Executing the Proof
Given the above facts, the following procedure is feasible to execute. It is a computer procedure, but the work involved is orders of magnitude smaller than the EDP proof, and the predicates needing to be checked are simpler than for the Four-Color Theorem.
- Generate -many sets of -many even numbers below .
- For each , for each , search for primes summing to .
- If each -case succeeds, accept and output the entire table of as the proof.
We could weaken the last step to accept if for a two-thirds majority of , every -case succeeds, but let us grant that the heuristic bounds on Goldbach’s Conjecture are good enough that this stricter and simpler policy has a high chance of success.
So granting that it succeeds and we get the output table—note that it is easy to verify afterward that the and are prime and sum to —as the “proof,” what do we really have? Define the statements as follows:
The statement says: “the set is indeed complementary for up to .”
The statement says: “the set has all its even numbers the sum of two primes.”
We claim that this fits our framework; let’s check. At least half the time . We suppose that some is a complement—we only need one. Let that is odd. Then where is a prime and is in . But we checked that is true, so all the are sums of two primes. This means that is proved.
One aspect is that if our routine failed, then we would have a significant “probabilistic” result of a completely different kind. It would indicate that the heuristic bounds on Goldbach’s Conjecture are incorrect. But once the routine succeeds, all that is water under the bridge. We have already proved each , and our routine has bypassed the need to prove , which would ostensibly be computationally prohibitive.
Note also that we are of course not assuming Goldbach is true overall—we are only needing to verify it for the tiny sample of numbers that go into each . That is, call “good” if is true, and “hyper-good” if every obeys the heuristic bounds on Goldbach. We don’t actually need to argue that with probability at least a random is hyper-good—once is checked the “hyper” part is dispensed with. Hence we only need that a random is good with probability at least . Then the confidence in being a proof is . Is that enough?
Comparing Other Probabilistic Proofs
Consider the problem of proving that a given arithmetic formula computes the zero polynomial over some finite field . Whenever does not compute the zero polynomial, a random subset of known small size will, with probability at least , include an argument giving . Now choose -many such subsets , and run a routine exhibiting that for every and . Let be the resulting table of zero values. (Of course, we could have just picked one random of size , but we are comparing with the above.) Is this exactly the same kind of “proof”?
We argue no. The main reason is that the statement corresponding to , namely that is “good,” is counterfactual. It is saying that if were a non-zero polynomial, then would have had a counter-example. The only way to avoid the problem of “which ?” seems to be for to be a universal hitting set for all non-zero -variable polynomials over . The size bounds on universal hitting sets, especially in arithmetical not Boolean complexity, are murkier to argue.
The cases of randomized algorithms for deciding primality and other problems in or (etc.) look similar. For a language in the Arthur-Merlin class , there is a predicate decidable in time such that for all :
Here we would want a bunch of pairs to be the proof of the theorem “.” By the perfect completeness theorem for , we can replace by such that the first line holds for all , which is analogous to the idea of our routine always succeeding and outputting a set of such pairs.
The problem again, however, is that the goodness of the pairs is still defined with respect to counterfactual cases. Whereas in our proof, goodness is a positive statement, namely that the randomly-chosen set really is complementary to the set of primes.
Open Problems
Is this a new type of proof? What should we call it? Are there novel applications of the method? Note that the size of the range is less important than having concrete density estimates on intervals, since the point is needing to check relatively few members.
Isn’t probabilistic proof an oxymoron?
I’m a little confused. You want to make a claim of the form:
Pr[Theorem = False| Proof succeeds] < 1/2^m
But you instead seem to argue something like:
Pr[Proof Succeeds | Theorem = False] < 1/2^m
To go from one statement to the other you would normally need to apply Bayes Rule, and to do that, you would need a prior belief about the theorem being true. How do you get around this difficulty?
Under the section titled Monte Carlo proofs, I think you need to be more explicit that the set of statements Ai, …, An are complete in a sense (i.e. there are no other statements that matter). This condition becomes clear in the example with the sets of numbers below C.
I would say that this does not constitute a proof. This exercise is similar to Bayesian inference. Each additional Ai you check becomes an experiment and it may strengthen your confidence further (or completely kill it).
Aren’t all proofs probabilistic? Pr[Reader_k believes what I wrote \forall k \in {1,..,12} | faulty proof] < 0.1% Two failed proofs of the four color theorem stood for 11 years.
Yes, I think this is a very nice concept and I would certainly call it a probabilistic proof. Nevertheless, as was pointed out by Story Donald, it does not prove that the theorem is true with 99% or anything like that, such statements don’t even make sense.
An example to understand why, imagine that we take a random 100 digit number. Then we run a primality test on it that returns “not prime” for any non-prime with 50% chance, otherwise says “possible prime”. Suppose we run this test 10 times, every time we get “possible prime”. Still, our number is more likely to be composite than prime.
But if we insert a theorem to such an algorithm, then it is either true or false, so we cannot assign a probability to it. But as Koray wrote, we can increase our confidence that it is true. So I think this is a nice concept and I wonder if it can be applied to other problems.
ps. I don’t really understand why you say it is different from RP.
Complementarity is defined as a two argument predicate: Q is complementary to P. But in the next sentence it’s used as a one argument predicate where it’s said that most sets of a certain size are complementary. What is the intended meaning?
Also confused by what the definition if C is here. Is complementarity a property whose definition changes as C varies?
Complementary to P is intended. Here “P” means the set of primes up to a certain C, so it changes as C does, although informally it’s always the set of primes.
On a slightly off-topic but related note, there exists something called a probabilistic checkable proof which is an interesting concept in itself. But a probabilistic proof itself is certainly something else.
This is one of the reasons I’m rather skeptical of any proof that isn’t in principle capable of being represented in first order logic; Granted, the execution of such a task is an enormous effort for modern mathematics, given much of modern mathematics beyond the graduate level has yet to be formalized, but most of it doesn’t face any theoretical barrier to formalization.
With a formal system and a proof, proof checking is mechanical and entirely verifiable, where your confidence in the proof is your confidence in the formal system and the verifier program. Proof verification programs can be very simple and are themselves rather easy to verify by accomplished engineers and mathematicians as correct, and we are fairly confident in formal systems such as first order logic today.
The feeling that the proof could be wrong because a computer is verifying it rather than even more fallible humans strikes me as misplaced. The risk that the proof verification code is wrong is a real risk to be sure, but its easier to find flaws in verification code than thousands of lines of a formal proof.
The risk of the code and formal system being wrong is when we’re using arguments from formal systems that we haven’t rigorously defined, such as running large amounts of calculations to search for a finite amount of counterexamples in a search space. What are the properties of the finite groups that map to the computer registers? What are the properties of the objects being represented by other facets of the code? Most of these aren’t rigorous compared to first order set theory, and wrong assumptions can lead to subtle traps of reasoning that could undermine the validity of the proof.
Betteridge’s law of headlines
Betteridge’s law of headlines is an adage that states: “Any headline which ends in a question mark can be answered by the word no.”
Dez Akin, a seminal document in regard to proof validation is the (collectively authored) “QED Manifesto“ (Automated Deduction, 1994). The ensuing 20 years have seen remarkable progress in that many thousands of fundamental theorems have been checked (by frameworks that include Mizar and Coq), and no serious challenges to the validity of accepted theorems have resulted. This finding is both remarkable and reassuring in regard to the logical integrity of the mathematical enterprise.
With regard to unsolved mathematical problems the situation is less satisfactory. The QED Manifesto envisioned that
For example, to date none of the main theorems of complexity theory have been formally verified in validation framework like Mizar and Coq (as far as I can tell). This lack is remarkable in view of the thousands of proofs contributed by other mathematical disciplines.
It is natural to wonder whether this lack of progress reflects not logical errors in the theorems of complexity theory — including complexity of simulation as a particularly important class of problems in complexity theory — but rather persistent uneasiness in regard to whether the starting postulates and definitions are ‘right’, in the sense of the QED Manifesto.
This foundational uneasiness is likely to persist — in some people’s minds anyway — for so long as our mathematics says so little that is both rigorous and useful in regard to lower-bounding the computational complexity of practical computations and simulations.
Conclusion There is scant likelihood the Gödel’s Lost Letter and P=NP will run short of thought-provoking material in regard to these “burning arrow“ issues in complexity theory!
Wow!
1. Yes, this is surely a proof, I do not understand the question mark in the title of this great post. Ok, formally this is not the full proof, but only because the calculation was not actually executed. If you would report that you actually performed the calculation with, say, m=100, and attach the full program code, this would surely be a proof.
2. This is one of the greatest proof in the whole history of mathematics: it resolves an important problem which had been open for almost 300 years using one great idea and a half-page of easy argument. In contrast, Helfgott’s paper is 79 pages long and full of complicated formulas. The full graduate course would probably needed to explain his proof to students. After this post, the proof of Weak Goldbach Conjecture can be explained to undegraduates in one lecture!
3. Yes, the idea should be new, otherwise the Weak Goldbach Conjecture would probably not be open until 2013. Except the main idea, the rest of agrument is straightforward…
4. With this proof, the Weak Goldbach Conjecture could anyway be wrong because of one the following reasons
a) one of the results you use contains an error, for example, 2002 reduction (by Liu Ming-Chit and Wang Tian-Ze) to the M=exp(3100) case is wrong; This is unlikely, but possible.
b) your proof contains an error. Yes, it is half-page only, and the program could be verified independently, so it is highly unlikely that it would contain an error everyone miss, but still possible.
c) ZFC is inconsistent, therefore the correctness of the proof does not imply the correctness of the Weak Goldbach Conjecture. This is much more unlikely than a) and b), but still possible.
In contrast, the event with probability 2^(-100) that your proof just happen to work by chance is so unlikely, that it could safety be treated as impossible, and thus it is not included in this list.
5. There are a lot of other important open problem reduced to finite search http://mathoverflow.net/questions/112097/important-open-problems-that-have-already-been-reduced-to-a-finite-but-infeasibl . Have you tried to apply your great method to any of them?
By the way, the “proving that a polynomial is zero” case is exactly like the first one – let A_i = (f = 0 or f(X) =/= 0). Then P(A_i) s always >= 1/2 not depending on f.
According to your link the new proof of the four-colour theorem is still uncheckable by human efforts.
Note that many things that mathematicians believe about math (or have confidence in or however you want to understand such affirmations and expectations) are not proven or unprovable like the consistency of arithmetic etc. The equation of proof with knowledge with mathematics creates a rather odd arrangement when compared to how we use the term knowledge in other fields.
Did anything happen grow out of this argument?
Dear domotorp:
No. Not heard anything.
Any idea?
Best and be safe
Dick