Reference textbook about proof techniques

Question

I am looking for some good recommended reference textbooks about proof techniques. Someone told me "G. Polya - How to solve it" is kind of standard, but quite old.

I am looking for a book that handles both classical (manual work) proofs and modern proof techniques using proof assistants or automated theorem provers. Or two separate books each handling just one of these topics.

Answer 1

The free book An Introduction to Proofs and the Mathematical Vernacular can be interesting. Quote from the author:

The typical university calculus sequence, which serves majors in the physical sciences and engineering as well as mathematics, emphasizes calculational technique. In upper level mathematics courses, however, students are expected to operate at a more conceptual level, in particular to produce "proofs" of mathematical statements. To help students make the transition to more advanced mathematics courses, many university mathematics programs include a "bridge course". Many texts have been written for such a course. I have taught from a couple of them, and have looked at numerous others. These various texts represent different ideas for what a bridge course should emphasize. Not having found a text that was a good fit with my own ideas, I decided to try to write one of my own. I am making the book freely available; a link is provided at the bottom of this page. But first I want to explain the ideas which I have tried to embody in the book.

Answer 2

I personally recommend Problem Solving Strategies

and Putnam and Beyond.

These are math-olympiad oriented. But I think they are excellent sources and they include loads of examples that are certainly not your average textbook problem.

Answer 3

On automated theorem proving, you can have a look at First-order Logic and Automated Theorem Proving by Mel Fitting. However, it is directed at an audience more mathematically sophisticated than typical readers of "introduction to rigorous math" books.

Answer 4

You have touched on three very different ways of viewing proofs and proof techniques:

• very general strategies for doing mathematics in general (homework or research).
• techniques used by automated theorem provers
• specific techniques for different mathematical domains

Very general strategies are covered informally in Polya and Velleman. These are things like forward vs backward proofs, divide and conquer, figuring out what your quantifiers are, generalization vs specialization. These are a must-have, they are both entertaining and informative, you'll be surprised at what you recognize and can now use consciously rather than stumbling on strategies that accidentally work. Also see the wikipedia article on mathematical proof.

But that is for doing proofs as a human. Automated deduction, finding proofs automatically, is very different. Here there is a lot of mathematical logic (proof theory) and computation. The 'strategies' discussed here are usually algorithms on specific kinds of data structures (manipulation of trees or formulas) which boil down to calculations, not on numbers, but on formulas. There is a lot of literature here on specific proof methods (predicate logic, tableaux, unification, induction, etc) and a lot of systems with each their own proof strategy (Coq (type theory), Isabelle (set theory and higher order logic, Hilbert style proofs). It's hard to give a single introductory text that says what the general techniques are because any text tends to be particular to its primary method. Also see the wikipedia article on automated deduction.

And then there are techniques specific to particular domains of mathematics. Proofs in old-fashioned Euclidean geometry (usually constructive) are very different from those in algebraic geometry (lots of algebraic manipulation). In some sense all (modern) math is about discovering very specific techniques in a domain to prove more facts in that domain. My point here is that though general techniques may help you solve your particular problem, don't lose the emphasis on the specific techniques already shown to be useful in that problem's domain. Also see the wikipedia article on ... well, math itself.

Just so you know, despite the obvious fact that most of the mathematical facts you know of are presented as algebraic manipulations, most of the math you don't yet know is discovered by looking at lots of examples and noticing a pattern.