
06539017
j
2016b.00478
Hipolito, In\^{e}s
What is a mathematical proof in the age of modern theorem provers?
Philos. Math. Educ. J. 29, 7 p., electronic only (2015).
2015
Professor Paul Ernest, University of Exeter, Graduate School of Education, Exeter
EN
E50
E20
D20
R40
mathematics and philosophy
foundations of mathematics
proving
proofs
formal proofs
mathematical logic
computerassisted proofs
mathematics and computers
modern theorem provers
odd order theorem
FeitThompson theorem
artificial agency
ontology
epistemology
research
http://socialsciences.exeter.ac.uk/education/research/centres/stem/publications/pmej/pome29/Ines%20Hipolito%20%20What%20is%20a%20Mathematical%20Proof%20in%20the%20Age%20of%20Modern%20Theorem%20Provers.docx
Summary: 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 fourcolour theorem in 1976, the status of proof has been widely discussed, and that discussion was recently reopened following the verification of the FeitThompson 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 FeitThompson 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.