Lean はマイクロソフトリサーチで開発された、依存型理論（dependent type theory）に基づく対話型証明支援系です。依存型理論はプログラムと証明の世界を結びつけます：したがって、Lean はプログラミング言語でもあります。Lean はその両面を重視していて、汎用プログラミング言語として使用できるように設計されています。ーー Lean は Lean 自身で実装されています。本書は、Lean でプログラムを書くことをテーマにしています。
プログラミング言語として見た場合、Lean は依存型を持つ正格（strict）な純粋関数型言語です。Lean でのプログラミングを学ぶには、これらの特徴がそれぞれプログラムの書き方に与える影響と、関数型プログラマのように考える方法を学ぶ必要があります。正格性（strictness）は、Lean における関数呼び出しが、ほとんどの言語と同様に機能することを意味します：つまり、関数本体の実行が始まる前に、引数が完全に計算されます。純粋性（purity）は、副作用を起こしうることがプログラムの型に明記されていない限り、Lean のプログラムがメモリ内で場所を変更したり、電子メールを送信したり、ファイルを削除したりといった副作用を起こしえないことを意味します。Lean は関数型言語であり、これは他の値と同様に関数が第一級の値であることと、プログラムの実行モデルが数式の評価から着想を得ていることを意味します。依存型（dependent types）は Lean の最も珍しい特徴であり、型すらも言語の第一級の部分にすることで、型がプログラムを含むことと、プログラムが型を計算することを可能にします。
本書は、Lean を学びたいが、必ずしも関数型言語を使ったことがないプログラマを対象としています。Haskell・OCaml・F# などの関数型言語に精通している必要はありません。一方、本書はループ・関数・データ構造など、ほとんどのプログラミング言語に共通する概念の知識を前提としています。本書は関数型プログラミングを学ぶ最初の一冊としては好適ですが、プログラミング全般を学ぶ最初の一冊としては不適切です。
Lean を証明支援系として使っている数学者は、いずれ自前の証明自動化ツールが必要になるでしょう。この本はそのような人たちのためのものでもあります。これらのツールは洗練されるにつれ関数型言語のプログラムに似てきますが、現役の数学者のほとんどは Python や Mathematica のような言語で訓練を受けています。本書は、より多くの数学者が保守可能で理解しやすい証明自動化ツールを書けるように、このような言語と関数型言語のギャップを埋める助けとなるでしょう。
本書は最初から最後まで直線的に、つまり飛ばさず読むことを意図しています。概念は1つずつ導入され、後の節は前の節を理解していることを前提としています。時には、先の章では簡単にしか触れなかったトピックについて、後の章で深く掘り下げることもあります。本書のいくつかの節には演習問題が含まれています。演習問題は、その節の理解を深めるために取り組む価値があります。また、本を読みながら Lean を実際に使い、学んだことを使う創造的な新しい方法を見つけることも有効です。
Lean のインストール
Lean でプログラムを書いて実行する前に、自分のコンピュータに Lean をセットアップする必要があります。Lean のツール構成は下記の通りです：
elanは、rustupやghcupと同様に、Lean のツールチェーンを管理します。
lakeは、cargo・make・Gradle と同様に、Lean パッケージとその依存関係をビルドします。
lean（シェルコマンド）は、個々の Lean ファイルを型検査し、コンパイルするだけでなく、編集中のファイルに関する情報をプログラマツールに提供します。通常、leanはユーザが直接呼び出すのではなく、他のツールによって呼び出されます。
- Visual Studio Code や Emacs などのエディタ用のプラグイン（拡張機能）は、
leanと情報交換し、その情報を便利な形で表示します。
Lean の最新のインストール方法については、Lean Manualを参照してください。
本書の書式
Lean に入力（input）として提供されるコード例は、このような書式とします：
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章に登場します。Unicode 文字により、Lean のコードは通常の数学的表記により近くなります。
デフォルトの Lean の設定では、Visual Studio Code でも Emacs でも、バックスラッシュ（\）の後に名前を続けることで Unicode 文字を入力することができます。例えば、α と入力するには \alpha とタイプします。Visual Studio Code で文字の入力方法を調べるには、マウスでその文字をポイントしてツールチップを見ればよいです。Emacs の場合、問題の文字をポイントしてから C-c C-k を使えばよいです。