The Hitchhiker's Guide to Logical Verification (2024 Edition)
by Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes HoĢˆlzl, and Jannis Limperg

lean

lean.forward

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.

Materials

Further_References