n-0/iteratecnextlean

A showcase for lean in formal verification.

iteratecnextlean (2023)

Welcome and thanks for choosing this workshop! I'm looking forward to dive right into the magical deep sea of interactive theorem provers (ITP) with you. Before we get on board, let's check if you have everything you need:

1. a computer (probably checked)
2. cloned this repository (probably checked)
3. Installed lean

Lean3 was a one-way installation while it's newest reincarnation lean4 (still unstable), has elan, a toolchain manager! (sth. like nvm or rustup [actually it's based on rust's manager]), allowing you to have multiple versions of lean. In most cases it's enough to have vscode with the lean4 (extensions)[https://marketplace.visualstudio.com/items?itemName=leanprover.lean4], which should get everything setup for you.

• install vscode extension
• Open this repository in vscode (having the extension installed)
• Open the file Tutorial.lean and continue!

For later

Here a helpful list of links related to lean (because Google has trouble finding it)

• Newer General overview/info/installation link
• Older General overview/info/installation, for lean 3 (but also lean4) (https://leanprover-community.github.io/)
• Github user related to lean link
• elan link
• lake (build tool/packet manager for lean, sth. like npm/gradle) link
• lean4 repository (compiler etc.) link
• Functional programming in lean4 (great official book) link
• Theorem proving in lean (great official book) link
• Mathlib 4 docs (but also includes docs for built in functions/macros/types like Bool, Prop, etc.) link
• Mathlib 3 docs link
• Zulip community link