PLUM: Mechanical Mathematicians
A mathematical claim is only accepted as valid if it is accompanied by a proof. Ideally, a proof should be a deduction from accepted principles that meets two requirements: on the one hand, it must strictly follow the rules of logical reasoning, but on the other hand, it should clarify why the claim had to be valid in the first place. When these two criteria come into conflict, the first takes priority. Some deductions, however, are so long or complex that they cannot be checked for errors by human beings. The success in designing computer systems to provide mechanical verification of the proofs of some famous theorems has led some mathematicians to suggest that all future proofs be written in computer readable code. A few mathematicians have gone so far as to predict that artificial intelligence will make human mathematicians obsolete.
Is mathematics a means to an end that can be achieved as well, or better, by a competent machine as by a human being? If so, what is that end, and why should we trust machines over humans? Or is mathematics rather an end in itself, pursued for its intrinsic human value? If so, what could that value be, and can it ever be shared with machines?