How To Prove It With Lean
by Daniel J. Velleman · Amherst College
Solves the hardest problem for a self-learner in this topic: with no grader, you cannot tell whether your proof is actually correct or merely feels correct. Lean answers that mechanically. Velleman's free companion has you re-do How to Prove It exercises inside the Lean proof assistant, which refuses to accept a gap. Machine checking exposes the hand-waving that a human grader often lets pass.
More resources on Introduction to Proofs
There's More to Mathematics Than Rigour and Proofs
The mental model that stops a learner from misreading this whole topic. Newcomers to proofs typically conclude that rigour replaces intuition and then stall; Tao's three-stage framing tells them what rigour is for and what comes after. Fields medallist's short essay on the pre-rigorous, rigorous and post-rigorous stages of mathematical development. Explains why formal proof exists at all: to destroy bad intuition and sharpen good intuition, not to replace intuition with symbol pushing.
How to Write Proofs: A Quick Guide
Ten-page guide from a Sheffield category theorist on the craft of writing a proof: planning before writing, what a proof must contain, common errors, and worked examples showing the gap between a correct idea and a readable argument. Its brevity is the point - it is the thing a learner actually rereads before submitting work.
