Computers and the Sociology of Mathematical Proof

Since the 1950s, computers have become ever more widely used to perform mathematical proofs. Mathematicians have used them for proofs (such as of the famous four-colour theorem) that are too extensive to conduct by hand. Automated proving is a fundamental technique of "artificial intelligence," and also central to debates about the very possibility of such intelligence. Computer scientists use automated theorem provers to verify the design of software critical to human safety or to national security, and "model checking" programs are now an important part of computer hardware design.

After reviewing briefly the history of these developments, the talk will explain why they are of interest to the sociology of scientific knowledge: they suggest the emergence of a set of "cultures of proving" different from those of ordinary mathematics. Clashes between cultures of automated proving and those of ordinary mathematics, and the first litigation centering on the meaning of mathematical "proof," will be examined. The talk will also discuss areas of tension within automated proving and outline a case in which the priorities of national security can be seen in the very construction of an automated theorem prover.