blanchette/logical_verification_2023

Hitchhiker's Guide to Logical Verification (2023 Edition)

Lean

119

13 commits

updated Nov 22, 2023

See the code

README

logical_verification_2023

Hitchhiker's Guide to Logical Verification (2023 Edition)

Installation

The Hitchhiker's Guide PDF document is generated from Lean files in the folder lean/LoVe. The same folder also contains an exercise sheet for each chapter.

To edit the Lean files, open the lean folder as a Lean 4 project as described here.

Contributors

blanchette

10 commits

JLimperg

3 commits

Similar repos

blanchette/logical_verification_2020

Companion files for Logical Verification 2020–2021 at VU Amsterdam

same org

blanchette/interactive_theorem_proving_2024

Files associated with the course Interactive Theorem Proving at LMU SoSe 2024

same org

leanprover/lean

Lean Theorem Prover

2,154

leanprover/vscode-lean4

VS Code extension for the Lean 4 programming language and theorem prover

313

b-mehta/formalising-mathematics-notes

Course notes for Formalising Mathematics 2026

129

leanprover-community/lean4-metaprogramming-book

311

clarksmr/sf-lectures

Software Foundations

161

PatrickMassot/GlimpseOfLean

An introduction to theorem proving in Lean for the impatient.

408

Languages

Lean

100.0%

blanchette/logical_verification_2023

Hitchhiker's Guide to Logical Verification (2023 Edition)

Lean

119

13 commits

updated Nov 22, 2023

See the code

README

logical_verification_2023

Hitchhiker's Guide to Logical Verification (2023 Edition)

Installation

The Hitchhiker's Guide PDF document is generated from Lean files in the folder lean/LoVe. The same folder also contains an exercise sheet for each chapter.

To edit the Lean files, open the lean folder as a Lean 4 project as described here.

Similar repos

blanchette/logical_verification_2020

Companion files for Logical Verification 2020–2021 at VU Amsterdam

same org

blanchette/interactive_theorem_proving_2024

Files associated with the course Interactive Theorem Proving at LMU SoSe 2024

same org

leanprover/lean

Lean Theorem Prover

2,154

leanprover/vscode-lean4

VS Code extension for the Lean 4 programming language and theorem prover

313

b-mehta/formalising-mathematics-notes

Course notes for Formalising Mathematics 2026

129

leanprover-community/lean4-metaprogramming-book

311

clarksmr/sf-lectures

Software Foundations

161

PatrickMassot/GlimpseOfLean

An introduction to theorem proving in Lean for the impatient.

408

Contributors

blanchette

10 commits

JLimperg

3 commits

Languages

Lean

100.0%