Sponsored by the Rutgers University Department of Mathematics and the
Center for Discrete Mathematics and Theoretical Computer Science (DIMACS)

Andrew Baxter, Rutgers University, baxter{at} math [dot] rutgers [dot] edu
Doron Zeilberger, Rutgers University, zeilberg {at} math [dot] rutgers [dot] edu

Title: Why Semi-Rigorous Proofs are at least as good as so-called Rigorous Proofs

Speaker: Doron Zeilberger, Rutgers University

Date: Thursday, February 19, 2009 5:00pm

Location: Hill Center, Room 705, Rutgers University, Busch Campus, Piscataway, NJ


Computer-Assisted and Computer-Generated Proofs took a long time to be accepted by the mathematical (at present predominantly human) community, but finally they did, although many people still think of them as inferior to purely human-generated proofs. The next frontier in the education of the mathematical human community is to convince them that semi-rigorous proofs (that with probability 100% could be made fully rigorous, with sufficient computing resources) are as good, if not better, than fully rigorous proofs (both of humans and computers), and it is a huge waste of time and money to find fully rigorous proofs.

The above opinion, first expressed in 1993 in my manifesto, recently became relevant in the recent proof, with my collaborators Manuel Kauers and Christoph Koutschan, entitled "A Proof of George Andrews' and Dave Robbins' q-TSPP Conjecture (modulo a finite amount of routine calculations)", that was submitted to the journal Seminaire Lotharingien de Combinatoire (SLC), and accepted only on the condition that the "misleading" title will be changed, since the editors and referees claim that we do not have a mathematically rigorous proof that the title is correct. They are right that we don't have such a mathematically rigorous proof, but they are wrong that the title is misleading. Consequently, we withdrew the article and it got accepted in a much more progressive journal.

The talk will discuss our seminal proof, whose importance far transcends the fact that it proves the most outstanding open problem in Enumerative Combinatorics. Its greater significance is in its format and computer-assisted and computer-generated methodology. At the end of the talk, I will try to explain, and symphatize with, the anachronistic views and sentiments of the editors and referees of SLC, that stem from the undeniable fact that they are mere human beings, and after all humans will be humans.