Numerous mathematicians and computer scientists are adapting computer systems to automate proofs, a computer process called automated theorem proving (ATP) or automated deduction, currently the most well-developed subfield of automated reasoning. In the 1970s, the first attempts were made to prove a theorem by computer. The so called four-color theorem was attempted by an ATP computer, which involved the theorem’s mapping problem: Using no more than four colors, the computer had to color regions of a map so that no two adjacent regions had the same color. Its proof relied on meticulous computer testing of many separate cases, all of which cannot be verified by hand.

Yet another more recent automated theorem prover is the Vampire, developed in the Computer Science Department at the University of Manchester by Andrei Voronkov and Kryštof Hoder (and previously with Alexandre Riazanov). To date, this ATP computer has won the “world cup for theorem provers,” also called the CADE ATP System Competition (International Conference on Automated Deduction [CADE], associated with the Association for Automated Reasoning) eleven times.

Although becoming less and less in numbers, some mathematicians (mostly purists) do not believe these computer-assisted proofs are valid. Not only could numbers be wrong, but the logic entered into the computer may not be correctly interpreted by the computer. They believe that only humans can understand the nuances and have the intuition needed to develop a theorem’s proof. But this is also often a proof’s dilemma: Many proofs would take decades—and reams of paper—to finish and prove, if you could prove them at all.