1. イントロダクション

1.1. 本書の始め方

本書のゴールは，対話的証明アシスタントLean4を用いて数学を形式化できるようになることです．これにあたって読者にはある程度数学知識があることを前提にしますが，それほど多くは必要ではありません．本書では数論から測度論，解析学までの内容を取り上げますが，ここではこれらの分野の初等的な側面のみに焦点をあてます．もし上記の中に馴染みのない分野があったとしても，順を追って本書を読み進めていくことで理解できることを期待しています．また，本書では形式手法の学習経験があることも前提としません．形式化は一種のコンピュータープログラミングと見なすことが出来ます:つまり数学の定義，定理，証明はプログラミング言語のように厳密な文法を持った言語で記述できます．こうすることによりLeanから様々な情報やフィードバックを得ることができます．与えられた式を解釈してその式が合法であることを検証したり，最終的に「証明の正しさ」を保証したりすることができます．

Lean project page や Lean community web pages から、leanについてのより詳細な情報を得ることができます．このチュートリアルはLeanの大規模で，今もなお成長し続けているライブラリである Mathlib に基づいています．また，もしまだ参加していないのでしたら， Lean Zulip online chat group に参加することを強く推奨します．ZulipはLeanマニアによるウェルカムで活気に満ちたコミュニティで，喜んで読者の質問に答えたり気持ちの面でもサポートをしてくれたりするでしょう．

本書はPDF版もしくはHTML版をオンラインで読むことができるようになっていますが，同時にVSCode内でLeanを実行しながら対話的に読めるようにも設計されています．

始め方:

  1. Lean4とVSCodeを installation instructions に従ってインストールします．

  2. git がインストールされていることを確認してください．

  3. instructions に従って mathematics_in_lean リポジトリをフェッチしてVSCodeで開いてください．

  4. 本書の各節には例や演習問題を含むLeanファイルが対応付けられています．これらのファイルは MIL フォルダ内に章ごとで格納されています．本書ではこのフォルダをコピーし，そこで動作確認や演習を行うことを強くお勧めします．これによりオリジナルのファイルはそのまま残り，リポジトリの変更に伴う更新も容易になります．（詳細は後述）読者はこのコピーに my_files 等の名前をつけ、これを使って新たに独自のLeanファイルを追加することもできます．

この時点で，以下のようにVSCodeのサイドパネルで本書を開くことが出来ます:

  1. ctrl+shift+P (Macの場合は command+shift+P )を押します．

  2. 上記手順で現れたバーで Lean 4: Docs: Show Documentation Resources と打ち込み，エンターキーを押します．（もしくはメニュー内で上記の文字列が選択されてハイライトされている場合はそのままエンターキーを押しても良いです．）

  3. これで開いたウィンドウで Mathematics in Lean をクリックします．

また，LeanとVSCodeを Gitpod を使ってクラウド上で実行することも可能です．この手順の説明がGithub上のMathematics in Leanの project page にあります．この方法で取り組む場合も，前述したとおり MIL フォルダをコピーすることをお勧めします．

本書とこれに関連するリポジトリは現在も開発中です．リポジトリを更新するには mathematics_in_lean フォルダ内で git pull と打ち込み，次に lake exe cache get を実行します．（この手順は MIL フォルダ内のコンテンツを変更していないことを前提としています．これがフォルダをコピーすることを推奨している理由です．）

MIL フォルダ内の演習問題は本書中にある解説や指示，ヒントを読みながら取り組むことを想定しています．また本書ではしばしば次のような例を記載しています:

#eval "Hello, World!"

本書で扱った内容のコード例が，リポジトリの対応するLeanファイルの中にあります．この行をクリックすると，VSCodeは Lean Goal ウィンドウ内にLeanによるフィードバックを表示し，また #eval コマンドにカーソルを合わせるとポップアップでこのコマンドに対するLeanの出力結果を表示します．試しにLeanファイルを編集して挙動を確認してみましょう．

本書はさらに挑戦し甲斐のある演習問題をたくさん掲載しています．しかし焦ってはいけません！Leanは数学を対話的に 実行する ためのものであり，読むためだけのものではありません．演習なしでは身につきません．全ての演習問題をこなす必要はありません．もし関連するスキルが身に着いたと感じたら，遠慮なく次に進んでください．そして読者はいつでも自身の解答と各節に関連する solutions フォルダにある解答とを見比べることが出来ます．

1.2. 概要

一言で言うならば，Leanは 依存型理論 （dependent type theory）と呼ばれる形式言語を用いて複雑な式を構築するためのツールです．

それぞれの式は 型 （type）を持ち，そしてそれは #check コマンドで表示することができます．例えば ℕ や ℕ → ℕ のような型があります．これらは数学的な対象です．

#check 2 + 2

def f (x : ℕ) :=
  x + 3

#check f

式の中には型として Prop を持つものも存在します．これらは数学的な命題です．

#check 2 + 2 = 4

def FermatLastTheorem :=
  ∀ x y z n : ℕ, n > 2 ∧ x * y * z ≠ 0 → x ^ n + y ^ n ≠ z ^ n

#check FermatLastTheorem

また式の中には Prop 型の式 P 自体を型としてもつものもあります．このような式は命題 P の証明です．

theorem easy : 2 + 2 = 4 :=
  rfl

#check easy

theorem hard : FermatLastTheorem :=
  sorry

#check hard

もしなんとかして FermatLastTheorem 型の式を構成でき，Leanに受け入れさせることができたら，とても素晴らしいことを成し遂げたことになります．（ここで sorry を使うのはズルで，Leanもそのことを知っています．）これでLeanがどういうものであるかわかったでしょう．あとはルールを覚えるだけです．

本書は同種のチュートリアルである Theorem Proving in Lean を補完するものです．[1] あちらはLeanの根幹にある論理フレームワークとコア構文についてより包括的に説明しています． Theorem Proving in Lean は新しい食洗器を使う前に取説を隅から隅まで読みたい人向けです．もし読者がとりあえず スタート ボタンを押してから食洗器内の洗浄ブラシがどう動くのかみてみたいタイプであるならば，本書から始めて必要に応じて Theorem Proving in Lean を参照する方が理にかなっているでしょう．

Mathematics in Lean と Theorem Proving in Lean のもう一つの違いは，本書では タクティク （tactic）の使用にずっと重点を置いていることです．Leanで複雑な式を作り上げたい時，2種類の方法があります:1つ目は式を直接書き下す方法．（これはテキストの記述に向いています）2つ目はLeanに式をどのように構成するかを 指示 する方法です．例えば以下の式は n が偶数なら m * n も偶数であることの証明を表しています．

example : ∀ m n : Nat, Even n → Even (m * n) := fun m n ⟨k, (hk : n = k + k)⟩ ↦
  have hmn : m * n = m * k + m * k := by rw [hk, mul_add]
  show ∃ l, m * n = l + l from ⟨_, hmn⟩

この 証明項 （proof term）は1行に圧縮することができます:

example : ∀ m n : Nat, Even n → Even (m * n) :=
fun m n ⟨k, hk⟩ ↦ ⟨m * k, by rw [hk, mul_add]⟩

以下は，同じ定理を証明項の代わりに タクティクスタイル （tactic-style）で証明したものです．ここで -- で始まる行はコメントで，Leanに無視されます．

example : ∀ m n : Nat, Even n → Even (m * n) := by
  -- Say `m` and `n` are natural numbers, and assume `n = 2 * k`.
  -- mとnを自然数とし，n=2*kと仮定．
  rintro m n ⟨k, hk⟩
  -- We need to prove `m * n` is twice a natural number. Let's show it's twice `m * k`.
  -- `m * n`がある自然数の2倍であることを証明する必要がある．そこで`m * k`の2倍であることを示す．
  use m * k
  -- Substitute for `n`,
  -- `n`を置換する．
  rw [hk]
  -- and now it's obvious.
  -- 後は明らか．
  ring

VSCode上でこのような証明の各行にカーソルを合わせると，Leanは 証明の状態 （proof state）を別画面に表示し，その時点までで証明をどこまで構築したか，そして目指す定理のためにあと何を示せばよいかを教えてくれます．また，Leanはカーソル位置での証明の状態を表示し続けるので，VSCode上で証明を一行一行たどることで，証明を追いかけることができます．この例では，証明の1行目で m と n （必要があればここで別の名前にすることもできます）を導入し，そして Even n を k と仮定 n = 2 * k の二つに分割しています．2行目の use m * k では m * n が偶数であることを m * n = 2 * (m * k) を示すことで証明していくと宣言しています．次の行では rewrite タクティクを用いてゴール中の n を 2 * k に置換しています．そして ring タクティクで m * (2 * k) = 2 * (m * k) を解いています．[2]

証明を組み立てるうえで，細かいステップごとに段階的にフィードバックを受けられることは，非常に役に立ちます．このため，タクティクを使うと証明項を書き下すよりも早く，簡単に証明を書くことができます．とはいえタクティクスタイルと項スタイルの間に明確な線引きは存在しません:上記の例の by rw [hk, mul_add] のように，項スタイルの証明の途中にタクティクスタイルの証明を入れることが可能です．そして反対に，この後見ていくようにタクティクスタイルの証明中で短い項による証明を用いるのが便利なこともよくあります．とはいえ，本書ではタクティクの使用に重点を置くこととしています．

上記のタクティクスタイルの証明例について，証明を一行にまとめることも可能です．

example : ∀ m n : Nat, Even n → Even (m * n) := by
  rintro m n ⟨k, hk⟩; use m * k; rw [hk]; ring

ここまで証明の小さなステップのためにタクティクを用いてきました．しかしタクティクで大幅な自動化も行うこともでき，長い計算と大きな推論ステップを正当化することができます．例えば，Leanの簡約化器である simp タクティクに，個別の簡約ルールとして偶奇についての命題を与えることで，同じ定理を自動的に証明することができます．

example : ∀ m n : Nat, Even n → Even (m * n) := by
  intros; simp [*, parity_simps]

本書と Theorem Proving in Lean の間のもうひとつの大きな違いは， Theorem Proving in Lean はLeanのコアと組み込みのタクティクのみに依存しているのに対し， Mathematics in Lean は Mathlib という発展を続ける強力なライブラリの上に構築されていることです．そのため，ライブラリにある数学的概念や定理，そして非常に便利なタクティクなどの使い方を紹介することができます．本書ではライブラリの完全な説明書として利用されることを意図していません;その代わりに コミュニティ のページに広範なドキュメントが掲載されています．むしろ，本書のゴールはライブラリにおける形式化の根底にある考え方を紹介し基本をおさえてもらうことで，ライブラリを自由に眺めて，その中から自力で必要なものを見つけられるようにすることです．

対話的な定理証明はなかなか思い通りにいかないものなので，学習曲線は険しいものになるでしょう．しかしLeanコミュニティは初心者をとても歓迎しており， Lean Zulip chat group では24時間体制で質問に答えています．そこであなたにお会いできることを楽しみにしています．きっとあなたもすぐに初心者の質問に答えたり， Mathlib の発展に貢献したりできるようになることでしょう．

そこで君のミッションを説明しよう: とにかくやってみて，演習問題に取り組み，Zulipで質問をし，そして楽しむことです．しかし先に警告しておきますが，対話的な定理証明は数学や数学的な推論について根本的に新しい考え方を迫るものです．あなたの人生は永久に変わってしまうでしょう！

Acknowledgments. We are grateful to Gabriel Ebner for setting up the infrastructure for running this tutorial in VS Code, and to Kim Morrison and Mario Carneiro for help porting it from Lean 4. We are also grateful for help and corrections from Takeshi Abe, Julian Berman, Alex Best, Thomas Browning, Bulwi Cha, Hanson Char, Bryan Gin-ge Chen, Steven Clontz, Mauricio Collaris, Johan Commelin, Mark Czubin, Alexandru Duca, Pierpaolo Frasa, Denis Gorbachev, Winston de Greef, Mathieu Guay-Paquet, Marc Huisinga, Benjamin Jones, Julian Külshammer, Victor Liu, Jimmy Lu, Martin C. Martin, Giovanni Mascellani, John McDowell, Isaiah Mindich, Hunter Monroe, Pietro Monticone, Oliver Nash, Emanuelle Natale, Pim Otte, Bartosz Piotrowski, Nicolas Rolland, Keith Rush, Yannick Seurin, Guilherme Silva, Pedro Sánchez Terraf, Matthew Toohey, Alistair Tucker, Floris van Doorn, Eric Wieser, and others. Our work has been partially supported by the Hoskinson Center for Formal Mathematics.