The Hitchhiker's Guide to Logical Verification is a textbook that introduces the reader to interactive theorem proving using the Lean 4 proof assistant as its vehicle. The textbook is accompanied by Lean demonstration and exercise files.
If you are an instructor and want to use the materials in your course, we would be grateful if you could contact Jasmin Blanchette.