README.org

Lean 4 Workshop

Overview

A hands-on workshop for learning Lean 4, the functional programming language and interactive theorem prover.

This repository contains:

• Learning resources and tutorials
• Example proofs demonstrating Lean 4 concepts
• Makefile for common operations

Quick Start

Prerequisites

• Lean 4 (v4.23.0 or later)
• Lake (comes with Lean 4)
• Optional: elan (version manager)

Check Your Setup

gmake deps    # Verify Lean 4 toolchain
gmake check   # Run a quick hello world test

Repository Structure

lean4-workshop/
├── README.org           # This file
├── RESOURCES.org        # Learning resources and tutorials
├── Makefile             # Build and check commands
├── lean-toolchain       # Lean version pinning
├── examples/            # Runnable examples
│   ├── satirical/       # Why specifications matter (5 files)
│   ├── correct/         # Proper specifications
│   ├── fp/              # Functional programming
│   │   ├── 01_OptionMonad.lean  # Option type and safe operations
│   │   ├── 02_IOMonad.lean      # IO and side effects
│   │   ├── 03_StateMonad.lean   # Stateful computations
│   │   ├── 04_TypeClasses.lean  # Polymorphism and overloading
│   │   └── 05_Recursion.lean    # Recursion patterns
│   ├── proofs/          # Theorem proving
│   │   ├── 01_Logic.lean        # Propositional logic
│   │   ├── 02_Equality.lean     # Equality and rewriting
│   │   └── 03_Induction.lean    # Inductive proofs
│   └── data/            # Data structures
│       ├── 01_Structures.lean   # Records and products
│       ├── 02_Arrays.lean       # Efficient arrays
│       └── 03_Inductive.lean    # Custom inductive types
├── exercises/           # Workshop exercises
│   ├── Ex01_Basics.lean          # rfl, simp, exact
│   ├── Ex02_NaturalNumbers.lean  # induction, arithmetic
│   ├── Ex03_Lists.lean           # list operations
│   └── Solutions/                # Complete solutions
├── .github/workflows/   # CI configuration
├── AGENTS.md            # Issue tracking instructions
└── .beads/              # Issue tracking database

Learning Path

1. Interactive Games (Recommended Start)

Game	Description	Link
Natural Number Game	Prove 2+2=4 and learn induction	Play NNG4
Set Theory Game	Learn set operations	Lean Game Server
Robo	Story-based math puzzles	Lean Game Server

2. Books and Tutorials

Resource	Audience	Link
Functional Programming in Lean	Programmers	FPIL
Theorem Proving in Lean 4	Proof enthusiasts	TPIL
Mathematics in Lean	Mathematicians	MIL
Learn X in Y Minutes	Quick reference	Lean4 in Y

See RESOURCES.org for the complete list.

3. Satirical Examples: Why Specifications Matter

The examples/satirical/ directory contains “O(1)” algorithms that satisfy weak specifications but don’t actually work:

Example	The Trick	Lesson
O1Sort	Identity function	Permutation spec must check elements
O1Search	Return first element	Must verify we found the TARGET
O1Hash	Return length	Determinism alone is useless
O1Compress	Return empty list	Must require decompression
O1Encrypt	Identity function	Reversibility without confidentiality

-- From examples/satirical/01_O1Sort.lean
def sort {α : Type} : List α → List α := id

-- WARNING: This is INTENTIONALLY WRONG!
def isPermutation : List α → List α → Bool
  | xs, ys => xs.length == ys.length  -- Only checks length!

The examples/correct/ directory shows how specifications should be written.

Moral: Formal verification proves your code matches your spec. It doesn’t prove your spec is what you actually wanted.

Editor Setup

VS Code (Recommended)

Install the lean4 extension from the marketplace.

Emacs

;; Using straight.el + use-package
(use-package lean4-mode
  :straight (lean4-mode
             :type git
             :host github
             :repo "leanprover-community/lean4-mode"
             :files ("*.el" "data")))

Key binding: C-c C-i toggles the proof state view.

Makefile Targets

Target	Description
help	Show available targets
deps	Check Lean 4 toolchain
check	Verify installation with hello world
build	Build project with Lake
clean	Remove build artifacts
verify	Verify all Lean files compile
verify-examples	Check satirical and correct examples
verify-exercises	Check exercises and solutions

Contributing

1. Fork the repository
2. Create a feature branch
3. Make your changes (org-mode files only)
4. Submit a pull request

Community

• Zulip Chat - Active, welcoming community
• Lean 4 GitHub - Source and issues
• Mathlib4 - Mathematics library

License

MIT License - See LICENSE file for details.

Acknowledgments

• Lean Prover Community
• Microsoft Research
• Workshop participants and contributors