33. Check proofs with proof assistants
Build small machine-checked proofs in a proof assistant and read the shape of larger formal libraries. This chapter covers tactics, definitions, lemmas, rewriting, and the modern push toward verified mathematics and software.