Opinion 112: On Human Hypocrisy (and Human-Centric Bigotry): A Typical Computer-Assisted Proof is Far More Rigorous (and Certain!, and Deeper!) than a typical Human-Generated Proof, (and some suggestions on how to improve the reliability of published mathematics in "peer"-reviewed journals)

By Doron Zeilberger

Written: Oct. 5, 2010 [Last update Nov. 2, 2010]

It took the Annals of Mathematics many years to finally accept, very reluctantly, Tom Hales' seminal, computer-assisted, article proving Kepler's 300-year-old conjecture, because they didn't trust computer proofs. It took them only a couple of months to accept a human-generated proof, by Daniel Biss, that was later found, by Nikolai Mnev, to be seriously flawed (and even though the error was pointed out more than five years ago, it took them about four years to publish a retraction). Annals editor Robert MacPherson looked at the bright side, commenting that "mathematics is self-correcting". I am not so sure, Professor MacPherson! For any crooked politician that has been caught, there are ten of them that have never (and will never) be caught. I am sure that there are many other humanly-generated Annals articles that are seriously flawed, because they were only checked by one or two human mathematicians, who would rather do their own research, and since they remain anonymous they are not accountable for their sloppy job.

If even the high-brow, pretentious, Annals of Mathematics contains flawed papers, I am sure that the middle-brow (but apparently equally pretentious) Proceedings of the American Mathematical Society (PAMS) contains even more incomplete proofs, and sometimes completely erroneous ones. After all, an average paper is read by at most two people (the author and the referee). Most people are so busy writing papers, that they don't have time to read them, and look for mistakes. Since the results published in the PAMS are not as "earth-shattering" as those published by the Annals, the motivation of people to find errors is very much reduced, and the referees, being anonymous, often do a very sloppy job.

On the other hand, a computer-assisted proof is far more reliable than any human proof, since such proofs are supported by reliable computer calculations, that in the hands of competent authors, are performed in several independent ways, and one can compare outputs. The probability of error, while strictly larger than zero, of course (after all the programming is still done by fallible humans), is much smaller than a traditional human-generated proof.

Hence, I was really disappointed when the Proceedings of the American Mathematical Society decided to reject a recent beautiful submission, by my brilliant student Andrew Baxter and myself, written in a lucid and engaging style, describing the ideas and methodology very clearly, but referring for the computational details to an accompanying webpage. Their decision was based on the report of a narrow-minded machino-phobic person, who apparently also believes that in order to be rigorous one has to be boring. The associate editor concurred with his (or her) decision stating:

"Under its current policy, PAMS accepts papers that present mathematics supported by proofs that meet traditionally accepted rigorous standards."

[Added Nov. 2, 2010: here is the full context]

What a joke! I am willing to bet that the computer-assisted proof by Andrew Baxter and myself is far more rigorous than ninety-nine percent of the human-generated papers published in the PAMS.

I am so sure that our proof is correct, that I am hereby offering $1000 for the first person to find a (non-trivial) error in the arguments, that would invalidate the formal correctness of the proof. The longer this offer will remain unclaimed the more rigorous our proof would be.

Let me take this opportunity to make three suggestion to the AMS to improve the very dubious reliability of its articles.

Another suggestion is to abolish the computer-assisted editing process that is very flawed. In fact, I found out about this unfortunate (and unjust, and of course, erroneous) decision to reject this masterpiece when I, quite by accident, clicked on the link given to me in April. All it said was "rejected". It turned out that the automated Email rejection message never reached me, due to our department's spam-filter, and Ken Ono told me that this is not the first case. Computers are great for discovering and proving non-trivial mathematics, but please, my dear editors, at least you owe it to me to get a personal human-generated rejection Email, rather than from a robot, that sometimes does not reach the recipient, and the poor author has the danger of never finding out, or finding out via the cryptic webpage.

But this is all minor compared to the great injustice, and bigotry, and hypocrisy, and human-centricity displayed by the editors and especially by the obnoxious machino-phobic referee. Welcome to the 21st century! Articles in scholarly journals should be chatty and exciting and describe the big picture. The certainty of this rejected paper is probably much higher than the certainty of any of that referee's papers. But, dear referee, suppose (only for the sake of argument) that there is an error somewhere, and you are unable (or unwilling) to check all the details of the computer program and the output. Big deal! The rejected paper had lots of beautiful ideas, and if you were less narrow-minded, and more enlightened, you would have taken a chance and recommend for publication this beautiful and insightful paper. Shame on you!

Added Oct. 19, 2010: Vince Vatter said that this cartoon reminded him of me.
Added Nov. 6, 2010: Watch the lecture
Added Feb. 4, 2011: We have just posted the second edition!
Opinions of Doron Zeilberger