Written: Mar. 7, 1996
In George Andrews's rejoinder ,`The death of proof? semi-rigorous mathematics? you've got to be kidding', (Math. Intell. 16(4) (Fall 1994), 16-18), to my semi-rigorous manifesto (Notices of the AMS, Oct. 1993, reprinted ibid., 11-14), he brings an example of a result that was found by computer (that the partial sum of Gregory's series, 4 arctan(1), taken at 500000 gives most of the digits of Pi to very high accuracy), but that required humans of the caliber of Borwein, Borwein, and Dilcher (Amer. Math. Monthly 96(1989), 681-687) to prove and explain.
This paper, winner of the Chauvenet prize, used by Andrews to proclaim Human Chauvinism(sic!), could have (essentially) been done by Maple, in one line, in less than a second of CPU time. This was pointed out to me today by Gert Almkvist (in an E-mail message whose main point was something else). The line is:
asympt(simplify( (sum(4*(-1)^(j-1)/(2*j-1),j=1..n/2)-Pi)/(-1)^(n/2+1)),n,11);
Try it!
So computers are great for discovering facts, but they are just as good at EXPLAINING them.
So instead of wasting our time proving things (or playing chess), let's dedicate our time to programming the computer to prove things. Myself, I find programming just as fun, and intellectually rewarding and challenging, as proving (or playing chess). So let's take pride, for some time, in our programming skills. Soon, of course, computers will also beat us there, and once they learn how to program, the race would be lost, since they would be able to teach themselves how to program to program. Then we would be able to wean ourselves of our competitive spirit, and do proofs (or programs) just for fun, like working out, or doing crossword puzzles.
Errata: Karl Dilcher has notified us that the paper discussed here is not the one that won the Chauvenet prize, but a paper by Bailey, Borwein and Borwein on Ramanujan's modular function and Pi, see his message to George Andrews.
For responses by George Andrews, Jon Borwein, Omar Foda, and Greg Kuperberg click here .