We presented how Graham's mathematical proofs on reasoning about programs can be encoded as Haskell programs and checked using Liquid Haskell. The proofs include equational reasoning for functional correctness, program optimization, and program calculation. The encoding from pen-and-paper proofs into machine checked proofs is direct, thus we claim that Liquid Haskell is a theorem prover that can be naturally used by all Haskell programmers.