Overview

The development of programmable electronic computers placed a powerful new tool in the hands of mathematicians. The computer's ability to manipulate symbols allows it to perform the same sort of rearrangements used by humans to solve equations. Early artificial intelligence programs were able to discover simple proofs in symbolic logic and geometry, and to solve some problems in calculus. In 1976 two University of Illinois mathematicians announced the computer-assisted proof of the famous conjecture that any map drawn on a sheet of paper could be colored with just four colors. This particular result, which required calculations more extensive than could be checked within a human mathematician's lifetime, raised a number of important questions about the nature and role of proof in mathematics.

Background

The first electronic computers were number "crunchers." Built during the Second World War and the...