# References and resources — Introduction to Lean

*Summer school "Proof assistants and applications", Strasbourg,
31 August – 4 September 2026.*

> **From the second day on, reopen your Codespace, do not create a
> new one.** The list of your Codespaces is at
> https://github.com/codespaces: click the one for `Strasbourg2026`
> to resume it, with your files and your work as you left them.
> Creating a second one starts from scratch.

## Before the first lecture

1. Use **Firefox**, **Chrome** or **Edge**
   (Safari is not recommended for Codespaces)
2. Create a (free) GitHub account if needed: https://github.com
3. Open the working environment:
   https://codespaces.new/xroblot/Strasbourg2026
   then click **Create codespace**
4. Wait for it to fully load (~5 minutes the first time)
5. Check: open `Part1.lean` and place the cursor on the line
   `#check 2` (line 51). The Infoview, on the right, should display
   `2 : ℕ`. (If the Infoview is not open, toggle it with
   **Cmd+Shift+Enter** on macOS, **Ctrl+Shift+Enter** on
   Windows/Linux, or through the command palette,
   `Cmd/Ctrl+Shift+P` → "Lean 4: InfoView: Toggle InfoView".)

> **Be patient while Lean loads.** When you open a file, Lean
> processes it in the background; orange/yellow bars in the left
> margin (and a spinner in the status bar) mean it is still working.
> Wait until they disappear before expecting goals or tooltips.
> Nothing is broken, Lean is just getting ready.

> **The terminal** sits at the bottom of the screen and is usually
> already open. If not: menu **Terminal → New Terminal**, or toggle
> the bottom panel containing it with **Cmd + J** on macOS,
> **Ctrl + J** on Windows/Linux, or toggle the terminal itself with
> **Ctrl + backtick** (that key is usually at the top-left of the
> keyboard, just below Esc). This one is the same on all platforms.

**Local installation** (alternative to Codespaces):

1. Install Lean (the `elan` toolchain manager and VS Code extension):
   https://lean-lang.org/install
2. In the terminal, clone this repository and enter it:
   ```
   git clone https://github.com/xroblot/Strasbourg2026.git
   cd Strasbourg2026
   ```
3. Download the prebuilt Mathlib cache
   (otherwise compiling Mathlib takes hours):
   ```
   lake exe cache get
   ```
4. Open the folder in VS Code and open `Part1.lean`. The first
   load takes a few minutes while Lean starts up.

**Fallback** (no installation): https://live.lean-lang.org

## Official sites

- **Lean**: https://lean-lang.org
- **Lean community**: https://leanprover-community.github.io
- **Mathlib** (thematic overview):
  https://leanprover-community.github.io/mathlib-overview.html
- **Mathlib documentation**:
  https://leanprover-community.github.io/mathlib4_docs/

## Learning Lean

- **Mathematics in Lean** (reference book):
  https://leanprover-community.github.io/mathematics_in_lean/
- **Natural Number Game** (interactive game):
  https://adam.math.hhu.de/#/g/leanprover-community/NNG4

## Going further — how Lean works

The interlude in `Part1.lean` sketches the pipeline (parser, macros,
elaborator, kernel) and why none of it has to be trusted. These are
the sources.

- **The Lean 4 Theorem Prover and Programming Language**, L. de Moura and
  S. Ullrich (CADE 2021) — the system description: parser, macro system,
  elaborator, kernel, tactic framework, compiler. The primary source.
  https://lean-lang.org/papers/lean4.pdf
- **Metaprogramming in Lean 4**, community book — chapter "Overview" follows a
  piece of code through `Syntax`, then `Expr`, then execution. The most
  readable account of the pipeline.
  https://leanprover-community.github.io/lean4-metaprogramming-book/main/02_overview.html

## History and background

- **The Proof in the Code: How a Truth Machine Is Transforming Math and AI**,
  Kevin Hartnett (Quanta Books, 2026) — the story of Lean and Mathlib, from a
  code-checking project to a library that changed how part of the mathematical
  community works. Journalism, not mathematics; no prerequisites.
  https://www.quantabooks.org/books/the-proof-in-the-code/

## Community

- **Zulip** (community forum): https://leanprover.zulipchat.com/