Will Mathematician Be Replaced by AI?

Theorem Provers

There are two different kinds of computer programs to prove theorems. One is automated theorem provers (ATPs) which perform prodigious computations, crunching out long sequences of logical steps leading from the axioms to the conclusions. Once written, they can work without any human intervention. They have been successful in proving some results. The other is interactive theorem provers (ITPs), which are used by mathematicians to assist in proofs. These proofs require a combination of creative thinking and meticulous mechanical reasoning. An ITP can carry out the laborious tasks, while the mathematician provides the creative insights. 

Computers have led to some important progress in mathematics: the four-colour theorem and Kepler’s conjecture both required intensive computation for their proof. But some mathematicians dispute these proofs, as reviewing those calculus programs is beyond human’s capacity. Another difficulty is that computers can generate proofs that are difficult or impossible to understand.

Controversy

There are still some controversies over the role of computers. There is no doubt that computers have played a role in checking proofs and in deciding on the validity of theorems submitted for publication. Many mathematicians are not that enthusiastic about computers, and they incline to the methods they have always been using. Even though they considered that some simple procedures in the process of proofing can be conducted in a mechanized way, they remain doubtful whether computers can generate interesting conjectures or not. They deem that the creativity is the characteristic of human beings fundamentally, which cannot be made in an automated fashion.