I finished Lockhart’s Lament, the 25-page version, and I have some feedback about it. On Proof I regard proof as being the defining activity of math. Really the trio of axiom-theorem-proof. However, proof is the real heart of the matter. I used to have a sort of mystical admiration for the idea of proof. Then Tyler taught me a little bit about Coq, the theorem prover, using Software Foundations. I learned that proof is always intended for an audience, and that the most objective audience wo...
