How Close Are Computers to Automating Mathematical Reasoning?

"They're this crazy contact between an imaginary, nonphysical world and biologically evolved creatures," said the cognitive scientist Simon DeDeo of Carnegie Mellon University, who studies mathematical certainty by analyzing the structure of proofs. "We did not evolve to do this." Computers are useful for big calculations, but proofs require something different. Conjectures arise from inductive reasoning -- a kind of intuition about an interesting problem -- and proofs generally follow deductive, step-by-step logic. They often require complicated creative thinking as well as the more laborious work of filling in the gaps, and machines can't achieve this combination. Computerized theorem provers can be broken down into two categories.