My advisor, Branden Fitelson, recently pointed me to a couple papers by Don Fallis about standards for proof in mathematics. In “Intentional Gaps in Mathematical Proofs” he points out that mathematicians very often (perhaps even almost always) publish results with only incomplete proofs. Even ignoring the fact that most of these proofs couldn’t be translated into a formal language in any reasonable way, people occasionally miss steps and give genuinely incorrect proofs, but also often intentionally leave out many steps. The latter occurs whenever words like “as one can easily see” or “as the reader can verify” occur, but also when appeal is made to a generally known theorem, especially “folk theorems” that are known by specialists but have never been proven (correctly) in print. These and related practices are generally accepted, though in some cases (like the computer proof of the four-color theorem, or the massively collaborative proof of the classification theorem for finite simple groups) there is some controversy because no human either has or could verify the whole thing. In fact, skipping steps in a proof is not just tolerated, but strongly encouraged, because it helps clarify the structure of the whole argument, and prevents the reader from getting bogged down in unilluminating details that take more time than insight to verify.

However, though mathematicians accept incomplete deductive proofs, they don’t accept probabilistic proofs. In “What Do Mathematicians Want?: Probabilistic Proofs and the Epistemic Goals of Mathematicians”, Fallis argues that there is no good reason for this prejudice. Any epistemic goals that deductive proofs can satisfy can also be satisfied by some probabilistic proofs, and any goal that rules out probabilistic proofs would rule out many seemingly acceptable deductive proofs as well. In particular, certainty is not better served by requiring deductive proofs – after all, it is far more likely that the several hundred (several thousand?) pages of dense, specialized work that together proved the classification of finite simple groups contain some mistakes, than that the two hundred-digit numbers generated probabilistically by an RSA algorithm are composite. There is possibility of error in both cases, and the probabilistic proof has one more potential source of incorrectness, but since the overall proof is much shorter, the possibility of error in the long and complicated deductive proof is greater.

I think Fallis overstates some of his point in this paper – a deductive proof can be rechecked many times, decreasing the likelihood of error arbitrarily far; for an inductive proof, to decrease the likelihood of error, one must do more work beyond verifying the parts of the proof that are already present (assuming the proof is complete, contra the other paper). This fact seems potentially relevant. In addition, extremely long and complicated deductive proofs are often considered questionable, like the proofs of the four-color theorem and the classification of finite simple groups. It’s true that they have been accepted while probabilistic proof have not, but for an already-established result, an exceedingly long and complicated deductive proof is no more likely to be published than a probabilistic one. When mathematicians seek new proofs of old results, they want the new proof to somehow be enlightening, revealing some new connection, or avoiding some complicated technology used in the old proof. Or the new argument should provide a better explanation, or suggest new generalizations, or apply new technologies from some other field. Probabilistic proofs are unlikely to do any of these, except avoid complicated technologies. So the choices of mathematicians may be rational after all.

However, I think Fallis’ apparent program to point out some fallibilities in existing epistemological practices in mathematics is quite interesting. Mathematicians would do well to reconsider whether or not they really do or should require complete deductive proofs of their results. They simultaneously seem to have higher and lower standards than their own rhetoric indicates they should.

Russell O'Connor(12:38:54) :The purpose of my work is to bring the rigour of mathematics to an even higher standard. The “Four Colour Theorem” that you cite has already been verified by a computer proof system, all the way down the the logical principals of the calculus of inductive constructions. These sorts of case studies brings confidence to the claim that in the (near) future mathematical proofs will require software verification before being accepted as valid.

Anthony Widjaja To(14:49:57) :Could you please clarify what you mean by “probabilistic proofs” here? I presume you didn’t mean probabilistic proofs in the sense of Erdos …

Kenny(03:04:51) :Ah, right. The example given by Fallis is Rabin’s method for probabilistically proving that a number is prime. Some theorem is established showing that for any n, if it is not prime, then at least 3/4 of the numbers less than n have some property that easily verifies that n is composite. By checking 10 such numbers pseudorandomly, we can show that n is prime with error probability only 1 in a million. There’s a chance of error, but it can easily be made very low – much lower than the chance of error in a long deductive proof of primality by trial division. (Technically speaking, this just means we can reduce P(positive|false), rather than P(false|positive) – that is, we reduce the likelihood, not the posterior. To calculate the posterior, we need to know the prior probability, which we can’t say much about, except that it might be on the order of 1/log n.)

I never learned too many Erdös-style proofs using the probabilistic method in graph theory, but I recall that all the ones I learned could have been phrased entirely as counting arguments rather than involving probabilities. I was told that some more complicated ones couldn’t be, but I haven’t seen any like that myself. Of course, all these arguments are perfectly deductively valid, despite the misleading name.

Note that Fallis doesn’t include verification of the Goldbach Conjecture for many different even numbers. This is because we have no idea what the distribution of counterexamples would be like if there were counterexamples. Thus, in this case we can’t even get the likelihood, let alone the posterior, so we can’t give any sort of relevant probabilistic argument.