A proof is a step-by-step logical argument that verifies the truth of a conjecture. It both establishes the validity of a statement and explains why it is true. In the 1970s, the late mathematician Paul Cohen, the only person to ever win a Fields Medal for work in mathematical logic, reportedly made the prediction that computers will eventually replace mathematicians when proving their theorems.
The debate over the role of computers in pure mathematics is an animated one. Mathematicians, logicians and philosophers have long argued over what part of creating proofs is fundamentally human.
Conjectures arise from inductive reasoning – a kind of intuition about an interesting problem – and proofs generally follow deductive, step-by-step logic. Deducing new truths about the mathematical universe always has a great amount of intuition and creativity, and the process of deduction ‒ with the unearthing of the unexpected and the discoveries of further new mathematical objects along the way ‒ is not a means to an end, that a computer can replace, but the end itself.
“The drive to mechanise proof and proof verification doesn’t strongly motivate most mathematicians as far as I can tell,” Columbia University mathematician and 2007 Clay Research Award receiver Michael Harris said.
“I can understand why computer scientists and logicians would be excited, but I think mathematicians are looking for something else.”