Computer proofs

Considerable attention has been drawn to the discovery and proof of mathematical theorems by computer.

Perhaps the first major result by a computer came in 1976, with a proof of four-color theorem, namely the assertion that any map (with certain reasonable conditions) can be colored with just four distinct colors for individual states. This was first proved by computer in 1976, although flaws were later found, and a corrected proof was not completed until 1995.

In 2003, Thomas Hales of the University of Pittsburgh published a computer-based proof of Kepler’s conjecture, namely the assertion that the familiar method

Continue reading Are humans or computers better at mathematics?