1. イントロダクション

1.1. はじめに

この本の目的は、Lean 4 インタラクティブ証明支援系を用いて数学を形式化する方法を教えることにあります。 ある程度の数学の知識を持っていることを前提としていますが、必要な知識はそれほど多くありません。 数論から測度論や解析学に至るまで様々な例を取り上げますが、それらの分野の基本的な側面に焦点を当てることで、もし不慣れであっても学びながら理解できるようにしています。 また、形式手法に関する予備知識も前提としていません。

形式化は一種のコンピュータプログラミングと見なすことができます。 すなわち、Lean が理解できる、プログラミング言語のような厳格な言語で数学的定義、定理、および証明を記述します。 その代わりに、Lean はフィードバックや情報を提供し、式を解釈してそれらが正しい形であることを保証し、最終的には我々の証明の正しさを認証してくれます。

Lean については、 Lean プロジェクトページ や Lean コミュニティのウェブページ でさらに詳しく知ることができます。 このチュートリアルは、Lean の大規模で日々成長を続けるライブラリ Mathlib に基づいています。 また、まだ参加していない場合は Lean Zulip のオンラインチャットグループ への参加も強くお勧めします。 そこでは、質問に快く答え、精神的なサポートも提供してくれる、活気に満ちた親しみやすい Lean 愛好者のコミュニティが見つかるでしょう。

オンラインで本書の PDF や HTML 版を読むことも可能ですが、本書は VS Code エディタ内で Lean を実行しながら対話的に読めるように設計されています。 始めるには:

  1. インストール手順 に従って、Lean 4 と VS Code をインストールしてください。

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

  3. 指示 に従って、mathematics_in_lean リポジトリを取得し、VS Code で開いてください。

  4. 本書の各セクションには、例や演習が含まれる対応の Lean ファイルがあります。これらは章ごとに整理された MIL フォルダ内にあります。元のファイルをそのまま残しておくため、またリポジトリ更新時の管理を容易にするために、ぜひそのフォルダのコピーを作成し、そのコピー上で実験や演習に取り組むことを強くお勧めします。コピーは my_files などお好きな名前にして、自分自身の Lean ファイルを作成する際にも利用できます。

その時点で、以下の手順に従って VS Code のサイドパネルで教科書を開くことができます。

  1. ctrl-shift-P (macOS では command-shift-P )を入力してください。

  2. 表示されるバーに 「Lean 4: Docs: Show Documentation Resources」 と入力し、ハイライトされたらすぐにリターンキーを押して選択してください。(ハイライトされたら、すぐにリターンキーを押して選択できます。)

  3. 開いたウィンドウで 「Mathematics in Lean」 をクリックしてください。

あるいは、Gitpod を使ってクラウド上で Lean と VS Code を実行することもできます。 その方法についての説明は、Github 上の Mathematics in Lean project page に記載されています。 なお、前述の通り、MIL フォルダのコピー上で作業することを引き続きお勧めします。

この教科書とそれに付随するリポジトリは、まだ作業途中の状態です。 mathematics_in_lean フォルダ内で git pull の後に lake exe cache get と入力することで、リポジトリを更新することができます。 (これは MIL フォルダの内容を変更していないことを前提としており、そのためコピーを作成することをお勧めしています。)

教科書には説明、指示、ヒントが含まれているので、その内容を読みながら MIL フォルダ内の演習に取り組んでいただくことを意図しています。 教科書には、しばしば以下のような例が含まれています。

#eval "Hello, World!"

対応する例は、関連する Lean ファイル内に見つけることができるはずです。 行をクリックすると、VS Code の Lean Goal ウィンドウに Lean のフィードバックが表示され、また、#eval コマンドにカーソルを合わせると、そのコマンドに対する Lean の応答がポップアップウィンドウに表示されます。 ファイルを編集して、自分自身の例を試してみることをお勧めします。

本書では、挑戦的な演習問題がたくさん用意されています。 これらを飛ばさず、しっかりと取り組んでください！Lean は、単に数学について読むだけでなく、対話的に数学を実践するためのものです。 演習問題に取り組むことが、この体験の中心となります。すべての問題に取り組む必要はありませんが、必要なスキルを習得したと感じたら、次の章に進んで構いません。 また、各セクションに付属する solutions フォルダの解答と、自分の解答をいつでも比較することができます。

1.2. 概要

簡単に言えば、Lean は 依存型理論 として知られる形式言語において、複雑な式を構築するためのツールです。

すべての式には型があり、 #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

ある式が型 P を持ち、なおかつ P 自身が型 Prop であるとき、その式は命題 P の証明となります。

theorem easy : 2 + 2 = 4 :=
  rfl

#check easy

theorem hard : FermatLastTheorem :=
  sorry

#check hard

もし型 FermatLastTheorem の式を構築し、Lean がそれをその型の項として受け入れたならば、あなたは非常に印象的な成果を達成したことになります。 ()``sorry`` を使うのはカンニングであり、Lean はそれを知っています。) これでゲームの流れは分かったはずです。あとはルールを学ぶだけです。

本書は、Lean の基盤となる論理的枠組みと基本構文について、より詳細な導入を提供する補完的なチュートリアル Theorem Proving in Lean と補完関係にあります。 Theorem Proving in Lean は、新しい食器洗い機を使用する前に取扱説明書を最初から最後まで読むのを好む人向けです。 もし、スタートボタンを押してから後でポットスクラバー機能の起動方法を確認するタイプの方であれば、まずは本書から始め、必要に応じて Theorem Proving in Lean を参照する方が理にかなっています。

Mathematics in Lean と Theorem Proving in Lean を区別するもうひとつの点は、ここでは タクティクス の利用に非常に重点を置いていることです。 複雑な式を構築しようとしていることを踏まえると、Lean はそれを行うための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⟩

証明項 は1行に圧縮することができます。

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

以下は、同じ定理の タクティクススタイル の証明です。 行の先頭が -- で始まる部分はコメントであり、Lean によって無視されます。

example : ∀ m n : Nat, Even n → Even (m * n) := by
  -- Say `m` and `n` are natural numbers, and assume `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`.
  use m * k
  -- Substitute for `n`,
  rw [hk]
  -- and now it's obvious.
  ring

VS Code でこのような証明の各行を入力すると、Lean は別ウィンドウに現在の 証明状態 を表示し、すでに確立された事実と、定理の証明のために残っている課題を示します。 カーソル位置での証明状態が常に表示されるため、各行を順にステップ実行することで証明を再生 (リプレイ) することが可能です。

この例では、まず証明の最初の行で m と n が導入され (必要であれば、この段階で名前を変更することもできます)、 また仮定 Even n を、ある k と n = 2 * k という前提に分解することがわかります。 次の行の use m * k は、m * n が偶数であること、すなわち m * n = 2 * (m * k) であることを示すことを宣言しています。 さらにその次の行では、rewrite タクティックを用いてゴール内の n を 2 * k に置き換え、 続いて ring タクティックが、結果として得られる m * (2 * k) = 2 * (m * k) というゴールを解決します。

小さなステップで証明を構築し、段階的なフィードバックを得る能力は非常に強力です。 そのため、タクティック証明は証明項よりも簡単かつ迅速に記述できる場合が多いです。 両者の間に明確な区別はなく、タクティック証明は証明項の中に挿入することができます (例えば、上記の例で 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 の簡約器 (simplifier) を呼び出すことで、定理を自動的に証明することができます。

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

両者の導入書のもう一つの大きな違いは、　Theorem Proving in Lean がコア Lean とその組み込みタクティックのみに依存しているのに対し、 Mathematics in Lean は Lean の強力で日々成長し続けるライブラリ Mathlib の上に構築されている点にあります。 その結果、ライブラリ内のいくつかの数学的オブジェクトや定理、そして非常に有用なタクティックの使い方を紹介することができます。 本書はライブラリの完全な概要を提供するためのものではなく、community のウェブページには充実したドキュメントが用意されています。 むしろ、我々の目標は、その形式化の背後にある思考スタイルを紹介し、ライブラリを自由に閲覧して自分で情報を見つけられるような基本的な入り口を示すことにあります。

インタラクティブな定理証明は、時にフラストレーションを感じさせ、習得のための学習曲線も急です。 しかし、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, Joseph McKinsey, Bhavik Mehta, Isaiah Mindich, Kabelo Moiloa, Hunter Monroe, Pietro Monticone, Oliver Nash, Emanuelle Natale, Filippo A. E. Nuccio, Pim Otte, Bartosz Piotrowski, Nicolas Rolland, Keith Rush, Yannick Seurin, Guilherme Silva, Bernardo Subercaseaux, 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.