1.1.1. 歴史（History）🔗

Leonardo de Moura は2013年に Microsoft Research 在籍時に Lean プロジェクトを立ち上げ、2014年6月16日に Lean 0.1 が正式にリリースされました。Lean プロジェクトの目標は、独立に実装可能な小さな論理カーネル提供する高い信頼性と、SMTソルバのようなツールの利便性と自動化を組み合わせ、同時に大規模な問題にも対応できるようにすることです。このビジョンは現在も Lean の開発の指針となっており、自動化の改善・性能の向上・使いやすさの向上に投資されています；信頼されたコアな証明チェッカもまた最小限で、独立な実装が存在します。

Lean の初期バージョンは主に C++ ライブラリとして構成され、クライアントコードが独立してチェック可能な信頼できる証明を実行できるようになっていました。この初期の数年間で Lean の設計は、最初は Lua で書かれたタクティクからのちに専用のフロントエンド構文へと、伝統的な対話型証明器へと急速に進化しました。2017年1月20日、Lean 3.0 シリーズの最初のリリースがありました。Lean 3 は数学者に広く採用され、自己拡張性を開拓しました：タクティク・記法・トップレベルコマンドはすべて Lean 自体で定義できます。数学コミュニティは Mathlib を構築し、Lean 3 の終わり頃には数学の形式化は100万行を超え、すべての証明が機械的にチェックされていました。しかしシステム自体はまだ C++ で実装されていたため、Lean の柔軟性には限界があり、必要とされるスキルが多岐にわたるため、開発はより困難になっていました。

Lean 4 の開発は2018年に始まり、2023年9月8日の4.0リリースで実を結びました。Lean 4 は重要なマイルストーンを体現しています：バージョン4の時点で、Lean はセルフホストされており、Lean を実装するコードの約90%は Lean で書かれています。Lean 4 の豊富な拡張 API は、必要な機能を追加するためにコアの開発者に依存するのではなく、ユーザに自分のニーズへ適応させる能力を提供します。さらに、セルフホスティングによって開発プロセスが大幅に高速化されたため、Lean の機能やパフォーマンスをより迅速に提供することができます；Lean 4 は Lean 3 よりも高速で、より大きな問題にも対応できるスケーラビリティを備えています。Mathlib は Lean の開発者がサポートするコミュニティの努力によって、2023年に Lean 4 への移植に成功し、現在では150万行を超えるまでに成長しました。Mathlib が50%増大したにも関わらず、Lean 4 は Lean 3 がその小さなライブラリをチェックするよりも早くチェックします。Lean 4 の開発プロセスは以前のすべてのバージョンを合わせたのと同じくらいの時間がかかりましたが、開発者たちはその設計に満足しています。これ以上の改修は予定されていません。

Leonardo de Moura と彼の共同設立者である Sebastian Ullrich は2023年7月、Simons Foundation International・Alfred P. Sloan Foundation・Richard Merkin からの後援を受けて、非営利団体 Lean Focused Research Organization (FRO) を Convergent Research 内に立ち上げました。FRO は現在10人以上の従業員を擁し、Lean やより広範な Lean コミュニティの成長とスケーラビリティの支援に取り組んでいます。

1.2.1. Lean のコード（Lean Code）🔗

本書には多くの Lean コードの例が含まれています。これらは次のような形式になっています：

コンパイラの出力（エラー・警告・単なる情報）は、コードの中と別に表示されます：

有益な出力、例えば Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling and evaluating it. * The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result. * If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m` to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`. Users can define `MonadEval` instances to extend the list of supported monads. The `#eval` command gracefully degrades in capability depending on what is imported. Importing the `Lean.Elab.Command` module provides full capabilities. Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly, since the presence of `sorry` can lead to runtime instability and crashes. This check can be overridden with the `#eval! e` command. Options: * If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances. * If `eval.type` is true (default: false) then pretty prints the type of the evaluated value. * If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance when there is no other way to print the result. See also: `#reduce e` for evaluation by term reduction. #eval の結果などはこのように表示されます：

"The answer is 4"

警告はこのように表示されます：

declaration uses 'sorry'

エラーメッセージはこのように表示されます：

application type mismatch
  Nat.succ "two"
argument
  "two"
has type
  String : Type
but is expected to have type
  Nat : Type

タクティクによる証明状態の存在は、以下の rfl の後のように、証明状態を表示するためにクリックできる小さな錠剤のようなマークの存在によって示されます：

証明状態は単独で示されることもあります。 2 + 2 = 4 を証明しようとするとき、最初の証明状態は次のようになります：

rflAll goals completed! 🐙 を使ったのち、結果の状態は次のようになります：

コード例中の識別子はそれのドキュメントに対してハイパーリンクが張られます。

構文エラーのあるコードの例は、エラーメッセージとともにパーサがどこで停止したかを示すインジケータを表示します：

def f : Option Nat → Type  | some 0 => Unit  | expected term=> Option (f t)  | none => Empty

<example>:3:4: expected term

1.2.2. 例（Examples）🔗

具体例は以下のように吹き出しの中に置かれます：

1.2.3. 専門用語（Technical Terminology）🔗

専門用語 とは、このようなリファレンスのような技術資料を書く際に、非常に特殊な意味で使われる用語を指します。 専門用語 の使用はこのようなリンクを使ってその定義位置にハイパーリンクされることがよくあります。

1.2.4. 定数・構文・タクティクの参照（Constant, Syntax, and Tactic References）🔗

定義・帰納型・構文形成器・タクティクには具体的な記述があります。これらの記述は以下のように記されています。

Even : Nat → Prop