Lean Book

Lean Book is the mdbook template configured for the Lean Project. Intended for use in writing textbooks and documentation in Lean.

Features

Lean Book has a variety of features.

Lean syntax highlighting works in this book. Here is an example of Lean code block.

variable {P Q : Prop}

example : P → (P ∨ Q) := by
  intro hP
  apply Or.inl
  exact hP

All Lean code blocks in this book have a button that jumps to the Lean Playground.

Jump to the Lean4 Playground by clicking on the play button in the top right corner of a page.

The markdown files in this book are generated from Lean code using mdgen. There is no need to maintain separately the code examples and the text.

The mdbook does not support searches in languages other than English, but this book does support searches in other languages (e.g. Japanese)!

You can use MathJax in this book. For example, $a^2 + b^2 = c^2$.

$$ ζ (s) = \sum_{n=1}^{\infty} \frac{1}{n^s} $$

Install mdbook and Lean.
Clone this repository. Do not fork to use this repository. Fork only when you want to submit a PR. Don't select "Use this template" on GitHub UI if you want your repository to be indexed by Reservoir.
Change the package name «Lean Book» as you like. And run lake update.
Change the site_url in book.toml to your GitHub page's URL.
Edit .lycheeignore file. This controls which URL is ignored by the link checker.
After updating the Lean file, run lake run build. This will generate markdown with mdgen, HTML with mdbook and import statements with import-check.
Run mdbook serve --open to see the preview.
Push to GitHub. The workflow for deploy has already been set up, so you can publish it as a web page by enabling deploy to GitHub Pages via GitHub Action from the repository settings.