Proving A Proof Is A Proof
How to convince someone your proof is really a proof
Roger Apéry was a mathematician who solved a beautiful problem that had been open for hundreds of years. He was not an amateur in any sense, but because his result was so surprising there was initial doubt about its correctness. Even professional mathematicians have some of the same problems that amateurs do.
Today I want to talk about how to know if your proof is a proof. And further how to convince others your proof is a proof. I have no magic single insight, but I have a few suggestions that I find useful, perhaps you will too.
Apéry proved that 
is the value of the famous “zeta” function 
Before Apéry ‘s work the status of
Ron Graham told me a story about the talk. It seems likely Apéry had a proof, but his presentation style and some of his comments—jokes?—did not make the audience feel confident in his claim.
Apéry ‘s proof depended on the following identity
At the time no one had seen such an identity. It was new. And it seemed magical—even the factor 
They grow in my garden.
You can imagine the effect such a comment might have on a group of skeptical mathematicians. If he had said:
The identity follows by using shifted Legendre polynomials. I can prove that all
It would have been okay. But “they grow in my garden” caused, according to Ron, many to start to leave the talk. However, someone in the back of the room had a programmable HP calculator, and quickly wrote a tiny program to check the identity. They interrupted the talk and said that the identity checked to the allowed accuracy of the calculator. Ron says this got everyone’s attention, and people sat back down and listened to the rest of Apéry ‘s talk.
In the years after the talk other mathematicians found proofs that were based on Apéry ‘s work. They were done and explained in a more conventional manner, and
Some Suggestions
I have a small collection of suggestions on how to know your proof is a proof. The same suggestions can be used to convince others, so I will concentrate on convincing yourself. In my opinion the last way to convince yourself or anyone else is to use formal methods. I have seen some comments in our discussions on using this or that formal system. I think that they have a role in mathematics, but not in the checking of a new result. See this for my thoughts on this topic: it’s an old paper with Rich DeMillo and Alan Perlis on the nature of proof.
I am suggesting that this be used to check some of your “lemmas” and claims. This approach does require a caution. Nature, especially in number theory, often will not reveal her secrets in small cases. I have already discussed a classic theorem of John Littlewood that showed that calculations can be misleading. But calculations can disprove a claim, even if they cannot prove a claim.
I have more than once thought that a false X was true and tried to prove it. In one case, after trying quite a while to prove such an X, I asked Philippe Flajolet for help. Philippe is a world expert on such problems. He used a combination of a technical insight I did not know and Maple to show why I could not prove X. The simple difficulty was there is a counter-example to X.
Lemma: For each integer
, the Euclidean space
has the red property.
I would suggest you check that 
I have discussed before work I did on the Vector Addition Problem. One false claimed proof that the problem was decidable had a lemma like the above. The lemma stated some property of Euclidean space 
A related issue is check any argument that handles a case X by saying: “the proof follows in the same way as case Y.” This is type of argument often relies on a symmetry between X and Y. But if the symmetry is missing, then X has not been proved. This happened years ago in a claimed proof that SAT needed super-polynomial size circuits. The claim was made by a world expert, and the bug was exactly of this type.
Imagine if Grigori Perelman had claimed the Poincaré Conjecture based on the Ricci Flow methods of Richard Hamilton. Yet when asked how he handled the “cigar” singularity suppose he had said,
the what singularity?
That would have raised lots of doubt about Perelman’s work. If you solve a problem, even a much more modest problem than Poincaré, you should know the difficulties that others have faced. And be prepared to explain how you overcame them, went around them, or through them—in general how you avoided them.
If someone says here is how I proved the Riemann Hypothesis: “it is a careful induction 
Say a set of complex numbers is a
-set if it can be covered by
set. First I show they are a
This sounds like it has a new idea, and while I need to see the details, I will listen. Even if the proof fails, there is some chance that the new ideas could be useful in solving other problems.
Suppose I am trying to prove some statement X. I may see an outline that looks like it will eventually lead to a proof of X. Often there are lots of details that have to be checked and lots of work to be done. However, sometimes I can see that if my method can prove X it could also prove another statement Y. This is a kind of “meta” argument, but I often find if a method proves X it will prove a related Y.
The key is then what is Y? If the statement Y is known to be false, then my method must fail. In this case I have avoided a great deal of work, and can use my time to refine my approach to X. If the statement Y is open, but considered likely to be false, then I may still continue. But now I am much more careful.
Another possibility is that the statement Y is a major open problem. Of course if my method will work this is great news, but usually I view it as showing my method is suspect. This does not make me abandon my approach; it does again make me very careful about each step. Almost always I find that I have a hidden issue in my approach in this situation.
Most of the false claims of famous open problems—I believe—have been single authored papers. Perhaps that is a lesson for us all.
Harry S. Truman once said:
It’s amazing what you can accomplish if you do not care who gets the credit.
Open Problems
Did these suggestions help? Do you have some additional ideas to help check proofs?
[fixed typo]
I haven’t finished reading, but you have a quick typo: the identity that Apery used should have (-1)^{n-1} in the numerator not (1)^{n-1}
There is a minus missing in the 5/2.. identity
Communicate in detail. See, e.g., Lamport’s How to write a proof: http://research.microsoft.com/en-us/um/people/lamport/pubs/lamport-how-to-write.pdf
I think the numerator inside the summation of zeta(3) should be (-1)^{n-1}.
I think the identity in the display above the “garden” quote is wrong. The factor of 1 to the n-1 probably should be -1 to the n-1.
All of these typos suggest a new post: How to Proof that your article on Proving a Proof is a Proof is Proving a Proof is a Proof. Alternately (shorter): How to Proofread an article on Proving a Proof is a Proof.
Even my own comment contains errors (darn lack of an edit button!). I will spare you all the joke of making the recursion even deeper.
Ross
Proof-reading is hard. That is for sure.
Thanks to all for pointing out the error. I wish I could say I had planned it, but it was a real misstake. I man mistake.
I have argued that Tarnlund has a proof of: P is not equal to NP.
The proof is in metamathematics, proof theory in the sense of Hilbert, about formal deductions (proofs) (deductions at the object level) in predicate calculus.
Thus, the proof itself is in the metatheory (proof theory) about the concept of formal deductions (proofs).
However, you are arguing: “In my opinion the last way to convince yourself or anyone else is to use formal methods. I have seen some comments in our discussions on using this or that formal system. I think that they have a role in mathematics, but not in the checking of a new result …”
Now, the statement: P is not equal to NP, has a proof in metamathematics about formal deductions. Then, the question arises, how do you express this proof, if you are not using the (informal) methods of metamathematics about formal deductions?
When Tarnlund has got the question: what is new here?
His usual answer is: axiom B i.e., a first order aximatization of a universal Turing machine of the mathematical theory of computing of Turing.
From this axiom there are propositional deductions (i.e., Turing machine computations) that by Robinson’s resolution give: SAT is not in P, by contradiction. There is an outline of the proof in this comment.
He often adds, the proofs use axiom B and some:
(i) Logic programming (Here, computing is a formal deduction (proof) from some assumption, which is a Horn clauses program, cf. Kowalski).
(ii) Mathematical logic, e.g., the concepts of formal deduction (proof) and proof theory, cf. Kleene.
(iii) Basic arithmetic in the metatheory, including limits.
(iv) Complexity results, e.g., Haken’s theorem on: Intractability of Resolution, and the Cook-Levin theorem: SAT is in P iff P = NP
“has a proof in metamathematics ”
It is a common mistake among non-mathematicians, and mathematicians not working in logic, to believe that there is a distinction between “mathematics” and “metamathematics”. There is no such distinction.
The statement “they grow in my garden” is a beautifully poetic description of where mathematical insights come from–and perhaps is something that Ramanujan would have agreed with as well.
I think that the commenter on the earlier post was on to something when he brought up using formal proof verifiers. Beginning programming students are taught that when they are trying to verify a piece of code that they’ve written, they should play the part of an interpreter and run through their code line by line, keeping track of all the variables. It can be a somewhat tedious exercise, but if there is a problem it will show students exactly where their code is doing something different from what they expected.
If someone is having trouble seeing if their proof has a hole in it, it might help them to play a mental game of being a proof verifier. It’s not necessary to go to the level of detail required by an actual formal verification–that might be similar to writing code in machine language–but anywhere a conclusion is drawn, the implied syllogism should be written out explicitly. This will force the author of the proof to spell out all of the assumptions that are being made, and to fill in some of the gaps that result from using natural language.
I don’t think this exercise would change the minds of some of the true believers that commented on the earlier post, but it should pretty quickly pinpoint where the problematic reasoning lies.
“They grow in my garden” is a great way of putting it. Recently I described the human mind to a few friends as a “Turing Machine with a ‘creativity’ oracle.” Douglas Hofstadter has an excellent bit about this “oracle” in his book Godel, Escher, Bach. He mentioned some results on timing savant computations – the time it takes savants to do the computations (even though they themselves describe the process of arriving at answers as ethereal or as ‘reaching into the platonic heavens’) grows in a way that agrees with known lower bounds. If memory serves, they tested addition and multiplication of n-bit numbers.
Another way to imagine this is to realize that many natural artifacts, even markets and networks or other complex interactions of isolated beings, have a high computational capability. It should be no surprise that the human mind, wired over billions of years to solve really tough problems really fast, is not an exception.
Unfortunately, I’m pretty sure we all run BPP code. Mathematicians (well, I guess pretty much everyone) should routinely ask themselves “Can I be wrong?” “Can I be wrong about this?” and “What have I done to validate that I’m not wrong about this?”
Additionally, Scott Aaronson has a pretty good post on something similar. He lists 10 heuristics that one might employ to weed out crank papers from legitimate papers. When self-applied, these heuristics might serve as additional lemmas on the road to proving your proof is a proof. (http://scottaaronson.com/blog/?p=304)
heh, from the title, I thought this post was going to be about Löb’s theorem.
According to section 3 of this 1979 article by Alfred van der Poorten
http://www.ega-math.narod.ru/Apery1.htm
the identity used by Apéry was known before.
There is a 1981 paper by Roger Apéry
“Interpolation de fractions continues et irrationalité de certaines contantes”
where he “gives an idea” as to how had arrived at his proof. The paper describes a transformation of the defining zeta 3 series into a continued fraction, which is then repeatedly transformed to get the desired convergence rate.
Both the first 1979 Apéry’s paper and the second one have no bibliography references.
Perhaps a research paper should provide such references. This is my opinion as amateur.
Great article! I really enjoyed reading it!
I believe that the most enthusiastic way of checking that a proof is correct is by using a powerful proof assistant, such as Coq. Its much harder than doing pencil and paper checking, but you end up having a binary file serving as a certificate of the proof’s correctness.
But bare in mind that this is a computer scientist’s point-of-view … 🙂
Cheers,
David Pereira
I just stumbled on your website because of the P=/=NP interest going around. It is mostly well thought out, and without silliness, but I have to object to your bringing up your old paper with DeMillo and Perliss. I might agree that formal proof is not the first thing to do in order to convince readers to believe your new proof, but that is for temporary practical resons (too hard to formalise Wiles’ proof), not for principled reasons as your paper claims. See my paper “How to Believe a Machine Checked Proof” for discussion:
http://www.brics.dk/RS/97/18/index.html
Randy Pollack