more on this theme | more from this thinker
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
| 10881 | The concept of 'ordinal number' is set-theoretic, not arithmetical [Horsten] |
| 10882 | Predicative definitions only refer to entities outside the defined collection [Horsten] |
| 10884 | A theory is 'categorical' if it has just one model up to isomorphism [Horsten] |
| 10885 | Computer proofs don't provide explanations [Horsten] |