by Daniel J. Velleman
ISBN: 0521675995
Buy on Amazon
Found in 7 comments on Hacker News
plinkplonk · 2014-12-04 · Original thread
Learn how to prove theorems. "How to Prove It" by Velleman is the best book for this (imho). (Amazon link http://www.amazon.com/How-Prove-It-Structured-Approach/dp/05...)

More good advice at http://scattered-thoughts.net/blog/2014/11/15/humans-should-...

jnazario · 2014-11-30 · Original thread
math IS hard. i didn't learn this until recently. i never met a practicing mathematician before a few years ago, and when i did they told me that they struggle to get stuff. that was a HUGE relief. if you enjoy it, then maybe you can apply yourself to it for the hours it may take to understand something - a book, a topic, a paper, etc.

i think a lot of what it comes down to for me - and maybe you - is mental discipline (staying focused for more than an hour without straying), knowing that it is very common for it to be tough, and learning how to play with math and explore it. i was never taught those things (or at least i never learned them), and so i have had to learn them the hard way. maybe you suffer from some of the same hurdles? try and overcome them, it's worth it.

as for writing proofs, one of those mathematicians got me interested in this book:

http://www.amazon.com/How-Prove-Structured-Approach-2nd/dp/0...

The principal thing I push learners towards after Haskell would be things like Coq and Agda. Coq has better learning materials, Agda has Haskell integration.

The usual sequence is [1] followed by [2].

Augment with [3] and [4] as needed.

One negative thing about Coq/Agda/Idris is they don't have a satisfactory encoding of typeclasses [5]. This is a problem in general with all dependently typed languages. Proof obligations get "churned" by changing code and the only tool to address that is extremely general proof terms combined with proof search. The best proof search is Coq, but the code extraction is heartburn-inducing for Haskell users.

Whereas in Haskell, we get extremely lightweight and type-safe code refactoring because of the way in which we leverage typeclasses and parametricity. This turns out to be very valuable as your projects get more serious.

That said, still entirely worthwhile to learn Coq or Agda.

By the way, this [6] is how I teach Haskell. Working on a book as well.

[1]: http://www.cis.upenn.edu/~bcpierce/sf/current/index.html

[2]: http://adam.chlipala.net/cpdt/

[3]: http://cheng.staff.shef.ac.uk/proofguide/proofguide.pdf

[4]: http://www.amazon.com/How-Prove-It-Structured-Approach/dp/05...

[5]: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceMa...

[6]: https://github.com/bitemyapp/learnhaskell

jfarmer · 2013-12-28 · Original thread
Polya's How to Solve It was recommended below. I also like How to Prove it by Daniel Velleman (http://www.amazon.com/How-Prove-It-Structured-Approach/dp/05...).
corey · 2013-09-08 · Original thread
Velleman's "How to Prove It" is a great book to learn how to do mathematics.

http://www.amazon.com/How-Prove-It-Structured-Approach/dp/05...

flatline · 2013-06-16 · Original thread
This is part of a series. I haven't read Solve It but there is another one that I worked through several years ago before returning to school, How to Prove It, that really cleared up how to do proofs for me. It is all based around set theory and some of the later proofs are quite deep:

http://www.amazon.com/gp/aw/d/0521675995/