The Babylonian vs. the Greek Approaches to Computer Proofs

By Doron Zeilberger

Delivered Dec. 14 2015

Videotaped lecture:

Abstract: Euclid, Aristotle, Plato and their friends gave us the wonderful formal logic and the axiomatic method that dominated Western mathematics for the last 2300 years. Automated Theorem Proving is a wonderful incarnation of this methodology for the computer age. However, we should also, in parallel, pursue the more naive, empirical and practical, Babylonian approach to mathematical knowledge, since being less "rigorous" (I am tempted to say "pedantic") , has the potential to go beyond the Greek straitjacket.

[This lecture was delivered on Dec. 14, 2015 at the Fields Institute's (Toronto) Workshop on Algebra, Geometry, and Proofs in Symbolic Computation organized by Georges Gonthier, Marie-Francoise Roy, and Eric Schost.

Personal Journal of Shalosh B. Ekhad and Doron Zeilberger

Homepage of Doron Zeilberger