Lean言語・形式証明系の普及を進めておられる北窓さんが執筆された本：
ゼロから始めるLean言語入門 ― 手を動かして学ぶ形式数学ライブラリ開発
を購入して読み進めています。
扱っている言語はLean4です。Lean4は多くの数学者にも使われ始めているのですが、今までにまとまった本はなく、公式サイトで配布されている資料や有識者の方が書いた資料をベースに勉強を進めるのが今までの学習方法でした。本書が日本語で出版されたことで、まずは本書から勉強を始めることができるようになり、大変嬉しいことだと思います。
購入はこちらから可能です。
ゼロから始めるLean言語入門 ― 手を動かして学ぶ形式数学ライブラリ開発 – 技術書出版と販売のラムダノート
上記のサイトは出版社のECサイトです。本記事執筆時点でここから購入するとこの本のPDF版(本来は有償)も付いてくるということで、大変お得になっているようです。詳細は上記ページでご確認ください。ちなみに本書はAmazon.co.jpでも購入可能ですが、その場合にはPDF版は付いてきません。私はうっかりAmazon.co.jpで購入したためPDF版は入手できませんでした、、、orz
この記事では、第６章まで読んだところでの感想を書いてみたいと思います。
Lean4は関数型プログラミング言語であり、かつ数学の形式証明アシスタントでもあります。このため全貌が大きく１冊の本で全てを紹介するのは難しそうです。全貌を書こうとすると
- Lean4の関数型言語としての特徴とプログラミング方法
- Lean4による数学の形式化、形式証明のための道具、その使い方
- Lean4で数学を進める方法
- Mathlib4に含まれる既存の定理の紹介とMathlib4の使い方
あたりは必要そうですが、本書はそこまで手を広げていません。２、３を中心に書かれていると思います。また必要に応じて１、４が書かれているような印象です。少し具体的に書いてみたいと思います。
本書では数学的題材としては自然数の構成（第７章、８章では整数の構成）を取り上げています。この題材は入門的な学習教材Natural Number Gameでも扱われているものですが、本書には入門学習教材にはない特徴があります。それは証明した基礎的な定理を後の証明で再利用できるようにする、という点です。
例えばLean4にはsimpというタクティクがあります。簡単な式変形を行ってくれる便利なタクティクで、Lean4組み込みの数（自然数、整数、実数など）の証明では頻出します。本書では独自実装の自然数を定義しているので、せっかく基礎的な命題（ゼロを足す、1をかけるなど）を証明しても、simpで活用されるわけではなく、rwタクティクで明示的に使う必要があります。
基礎的な命題をsimpタクティクに使ってもらえるようにLean4に登録すると、simpが独自実装の自然数でも動作するようになり、証明をどんどん進めることができるようになります。本書ではこの登録の仕組みや登録した定理の使い方など証明の再利用の説明について力を注いでいる印象を受けました。
また同じ証明を繰り返し書くことをできるだけ避けるために、普通は定理や補題としてまとめて、それを繰り返し利用するわけですが、もう少しプログラミング的な道具としてマクロという道具もあります。複数のタクティクをまとめて一つのマクロにすることで簡単に道具を増やすことができます。本書ではマクロの作り方、使い方の説明もあり、とても有り難かったです。自分で資料を見て勉強するのはちょっと面倒なところでも、日本語で例題付きの解説があると本当に敷居が低くなります。
数学の本を読んでいると数学の証明を進める上で「以下同様」とか「すでに群をなすことを示したので」とか、「を繰り返せば自明」とかのフレーズをよく見ます。Lean4でその部分をうまく処理できないと、同じような証明を何度も書くはめに陥ります。Lean4ではそのために、
- simpなど自動証明タクティクへの登録
- 型クラスを使った「よくある性質」の登録
- マクロによる自動化
などを始めとする様々な道具立てを用意しています。本書ではサブタイトルにある「数学ライブラリ開発」のために意識してこれらについて丁寧に説明されていると思いました。
これからさらに７章、８章に読み進めていく予定です。そこで本書の別の面白さが見つかれば記事にしようと思います。
