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.