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
Discrete Mathematics: An Open Introduction
A free, open-licensed undergraduate textbook covering counting and combinatorics, sequences and recurrence relations, symbolic logic, proof techniques including induction, and graph theory, with many worked exercises. Readers build the discrete foundations needed for computer science and upper-level mathematics.
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.
Introduction to Mathematical Thinking
Stanford course by Keith Devlin on how mathematicians reason, starting with the logic of language (and, or, not, implication, quantifiers) and moving to the structure of proofs, including contradiction and induction. Learners become able to read, construct and critique simple mathematical proofs.