A book on Lean 4 as a theorem prover (as opposed to a programming language).