Abstract
A mathematical proof is notable for its clear language which satisfies the logical rules of inference and which convinces us by its intrinsic explanation relatively easy to reproduce. Nevertheless, since the publication of the computer aided proof of the four-colour theorem in 1976, the status of proof has been widely discussed, and that discussion was recently reopened following the verification of the Feit–Thompson theorem by a modern theorem prover. Modern theorem provers enable us to verify mathematical theorems, construct formal axiomatic derivations of remarkable complexity and, potentially, increase confidence in mathematical statements. Proof assistants, therefore, are the result of the efforts by logicians, computer scientists, and mathematician to obtain complete mathematical confidence through computers. In this paper, I will discuss how classical mathematical theorems strongly contrast with the “trivial” use of modern theorem provers. I will specifically address the Feit–Thompson theorem, proof of which was recently verified by the interactive theorem prover Coq in order to assess the proof’s status in the era of modern theorem provers, and, more clearly, whether a machine proof may still be considered a calculus of reasoning.
