id: 06539017
dt: j
an: 2016b.00478
au: Hipolito, Inês
ti: What is a mathematical proof in the age of modern theorem provers?
so: Philos. Math. Educ. J. 29, 7 p., electronic only (2015).
py: 2015
pu: Professor Paul Ernest, University of Exeter, Graduate School of Education,
Exeter
la: EN
cc: E50 E20 D20 R40
ut: mathematics and philosophy; foundations of mathematics; proving; proofs;
formal proofs; mathematical logic; computer-assisted proofs;
mathematics and computers; modern theorem provers; odd order theorem;
Feit-Thompson theorem; artificial agency; ontology; epistemology;
research
ci:
li: 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
ab: 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 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.
rv: