1
vote
0answers
440 views

Arguments against Reductio ad Absurdum [closed]

Could Reductio ad Absurdum not be consireded a valid proof method? Are there any compelling arguments against it, or at it's favor? I feel like I am assuming some metamathematical hypothesis about my ...
19
votes
1answer
1k views

Community experiences writing Lamport's structured proofs

About two years ago, I came across this paper by Lamport http://research.microsoft.com/en-us/um/people/lamport/pubs/lamport-how-to-write.pdf on writing proofs hierarchically. It changed how I wrote ...
32
votes
15answers
6k views

Strong induction without a base case

Strong induction proves a sequence of statements $P(0)$, $P(1)$, $\ldots$ by proving the implication "If $P(m)$ is true for all nonnegative integers $m$ less than $n$, then $P(n)$ is true." for ...
9
votes
3answers
953 views

Is formal proof (formalized mathematics) interesting to practicing mathematicians? To educators? [closed]

Formalizing mathematical proofs so that they can be checked for correctness and manipulated by computer is a recurrent proposal, most notably stated in the QED manifesto (1994). The December 2008 ...