more from this thinker | more from this text
Full Idea
Mathematicians are uncomfortable with computerised proofs because a 'good' proof should do more than convince us that a certain statement is true. It should also explain why the statement in question holds.
Gist of Idea
Computer proofs don't provide explanations
Source
Leon Horsten (Philosophy of Mathematics [2007], §5.3)
Book Ref
'Stanford Online Encyclopaedia of Philosophy', ed/tr. Stanford University [plato.stanford.edu], p.26
| 17967 | To decide some questions, we must study the essence of mathematical proof itself [Hilbert] |
| 17627 | It seems absurd to prove 2+2=4, where the conclusion is more certain than premises [Russell] |
| 10256 | For intuitionists, proof is inherently informal [Shapiro] |
| 9646 | There is no limit to how many ways something can be proved in mathematics [Brown,JR] |
| 9647 | Computers played an essential role in proving the four-colour theorem of maps [Brown,JR] |
| 10692 | Hilbert proofs have simple rules and complex axioms, and natural deduction is the opposite [Beall/Restall] |
| 10885 | Computer proofs don't provide explanations [Horsten] |