Introduction to Formal Verification & Proof Assistants

A 10-Week Journey into Formal Verification with Lean4 (Spring 2026)

GDG @ AUB Software Team × AUB Math Society

PROOF101

Installing the Lean4 proof assistant

The VS Code extension provides the best experience for working with Lean4:

  1. Install VS Code: Download from https://code.visualstudio.com/
  2. Install the Lean4 Extension:
    • Open VSCode (recommended: VSCodium instead of VSCode, but they are functionally the same)
    • Go to Extensions (Ctrl+Shift+X / Cmd+Shift+X)
    • Search for “Lean4”
    • Click “Install”
  3. Follow the setup wizard that appears automatically
  4. Verify installation: Open a .lean file and check that syntax highlighting works

Full (official) installation guide: https://lean-lang.org/lean4/doc/setup.html

Alternative: Online Environment

For quick experimentation without installation:

Lean4 Web: https://live.lean-lang.org/

Note: The online environment is great for trying Lean4, but for the course assignments, we strongly recommend installing locally for the full development experience.

In fact, the online environment is amazing for live coding sessions and is quite good for prototyping and sharing Lean4 code with other people over the Internet. However, our recommendation is still to use a local installation for more serious and demanding tasks.