Leanはマイクロソフト・リサーチで開発された，dependent type theory (従属型理論) に基づく対話型証明支援系です．従属型理論はプログラムと証明の世界を結びつけます：したがって，Lean はプログラミング言語でもあります．Lean はその両面を重視していて，汎用プログラミング言語として使用できるように設計されています．ーー Lean は Lean 自身で実装されています．本書は，Lean でプログラムを書くことをテーマにしています．
プログラミング言語として見た場合，Lean は従属型を持つ strict (正格)な純粋関数型言語です．Lean でのプログラミングを学ぶには，これらの特徴がそれぞれプログラムの書き方にどのような影響を与えるか，そして関数型プログラマがどのように考えるかを学ぶ必要があります．正格性は，Lean における関数呼び出しが，ほとんどの言語と同様に機能することを意味します：つまり，関数本体の実行が始まる前に，引数が完全に計算されます．純粋性は，型で明記されていない限り，Lean のプログラムがメモリ内で場所を変更したり，電子メールを送信したり，ファイルを削除したりといった副作用を起こさないことを意味します．Lean は関数型言語であり，ほかの関数型言語と同様，関数は第一級の値であり，数学的な式の評価から実行モデルの着想を得ています．依存型は Lean の最も珍しい特徴であり，型を言語の第一級の部分にすることで，型がプログラムを含み，プログラムが型を計算することを可能にします．
本書は，Lean を学びたいが，必ずしも関数型言語を使ったことがないプログラマを対象としています．Haskell, OCaml, F# などの関数型言語に精通していることは必須ではありません．一方，本書はループ・関数・データ構造など，ほとんどのプログラミング言語に共通する概念の知識を前提としています．本書は関数型プログラミングの最初の一冊としては好適ですが，プログラミング全般の最初の一冊としては不適切です．
Lean を証明アシスタントとして使っている数学者は，いずれ自前の証明自動化ツールが必要になるでしょう．この本はそのような人たちのためのものでもあります．これらのツールは洗練されるにつれ関数型言語のプログラムに似てきますが，現役の数学者のほとんどは Python や Mathematica のような言語で訓練を受けています．本書は，より多くの数学者が保守可能で理解しやすい証明自動化ツールを書けるように，そのギャップを埋める助けとなるでしょう．
本書は最初から最後まで，直線的に読むことを意図しています．概念は1つずつ導入され，後のセクションは前のセクションを理解していることを前提としています．時には，先の章では簡単にしか触れなかったトピックについて，後の章で深く掘り下げることもあります．本書のいくつかのセクションには練習問題が含まれています．演習問題は，そのセクションの理解を深めるために取り組む価値があります．また，本を読みながら Lean を探求し，学んだことを使う創造的な新しい方法を見つけることも有効です．
Lean のインストール
Lean でプログラムを書いて実行する前に，自分のコンピュータに Lean をセットアップする必要があります．Lean のツール構成は下記の通りです：
elanは Lean のツールチェーンのインストーラで，rustupやghcupと同様です．
lakeは，cargoやmake, Gradle と同様に，Lean パッケージとその依存関係をビルドします．
Leanは，個々の Lean ファイルを型チェックし，コンパイルするだけでなく，プログラマ・ツールに現在書かれているファイルに関する情報を提供します．通常，Lean はユーザが直接呼び出すのではなく，他のツールによって呼び出されます．
- Visual Studio Code や Emacs などのエディタ用のプラグインで，
leanと通信し，lean の情報を便利に表示することができます.
Lean の最新のインストール方法については，Lean のマニュアルを参照してください．
表記法
Lean に入力として提供されるコード例は，このような書式とします：
def add1 (n : Nat) : Nat := n + 1
#eval add1 7
上の最後の行（#evalで始まる行）は，Lean に答えを計算するように指示するコマンドです．Lean の返事は以下のような書式とします：
8
Lean が返すエラーメッセージは下記のような書式とします：
application type mismatch
add1 "seven"
argument
"seven"
has type
String : Type
but is expected to have type
Nat : Type
警告は次のような書式で表示します：
declaration uses 'sorry'
Unicode
慣用的な Lean コードは，ASCII には含まれないさまざまな Unicode 文字を使用します．例えば，ギリシャ文字の α や β，矢印の → が，いずれも本書の第1章に登場します．これにより，Lean のコードは通常の数学表記により近くなります．
デフォルトの Lean の設定では，Visual Studio Code も Emacs も，バックスラッシュ(\)の後に名前を続けることでこれらの文字を入力することができます．たとえば α と入力するには \alpha とタイプします．Visual Studio Code で文字の入力方法を調べるには，マウスをその文字に向けてツールチップを見ればよいです．Emacs の場合，C-c C-k を問題の文字にポイントして使います．