Programming Proof

"Computers ought to produce in the long run some fundamental change in the nature of all mathematical activity.” These words, penned in 1958, capture the motivation behind an early field of computing research called Automated Theorem-Proving. Practitioners of this field aimed to program computers to prove mathematical theorems or to assist human users in doing so. Everyone working in the field agreed that computers had the potential to make novel contributions to the production of mathematical knowledge. There was disagreement about almost everything else including what ought to count or not count as a proof, how people prove theorems, and what computers could ultimately make possible in mathematics. This discussion will introduce approaches to automated theorem-proving with an eye to discussing the role of material culture in the history of mathematical knowledge production.