I have a question about proofs. While reading proofs I would sometimes encounter a step that I just don't get. I can verify that it follows from the previous steps and is correct, but not why it was taken. It just seems arbitrary. The question is: do mathematicians usually have a reason for these steps that they do not include in a proof, because it has no place in the formalism, or are these steps just the result of sudden revelations and random ideas and even the proof's author does not know why the proof is correct, only that it is? Do mathematicians "think in proofs" or is there a difference between what is written down as a proof and how it was conceived?
You think in conjecture and wonder how it's proved is my impression.
Lots of stuff in "How to Solve It" shows this.
TBH I mostly think in "how do I get ansible to read this yaml file I wrote."
You're reading wrong. You should always prove the theorems yourself before reading the given solution. >>2 has a good suggestion, The Psychology of Invention in the Mathematical Field is also decent on this topic and so is Proofs and Refutations. To me proof is the process of deconstructing a problem into a formally-inspired but intuitive understanding so that epiphany can happen later. There's more, but this is a good bit.
>>1 What should be in a proof is something not even all mathematicians agree on. Constructivists, in particular, only allow proofs with things that can be constructed- no infinities, no excluded middle, no proofs by contradiction.
At first Constructivism was seen as a threat by a lot of non-constructivist mathemeticians, but then even non-constructivist began to think that even if you are OK with a proof that says "There is a number that ..." it is nice to have another proof of the form "Here is a number that ..."
The Mathematical Experience by Philip J. Davis and Reuben Hersh covers this and a lot of other philosophical/historical issues on math.
No proofs by contradiction
What's wrong with those?
I remember looking at How to Solve It, since it was recommended at the end of The Little Schemer, isn't it just a collection of heuristics? Does that mean that mathematicians just randomly throw ideas at a problem to see what sticks? Or do they actually know why a proof works?
>>5
They reject the law of excluded middle because there are some logical paradoxes involving it. Interestingly all proof engines I'm aware of use constructivist math.