最近私のマイブームになっている Lean Prover というプログラミング言語兼証明アシスタントについて，それがどうして魅力的に思えるのか書いていこうと思います．
このブログの他のすべての記事と同様，すべて私の勝手な意見であることをご承知おきください．
あと，Lean 以外の証明アシスタントが存在することも承知していますが，私はそんなに詳しくないので「証明アシスタント」と Lean を区別せずに話をします．
- 論文の査読プロセスが変わる
- 数学を学習するのが容易になる
- 数学を独学できるようになる
- 数式処理システムとシームレスに連携できる
- Lean の UI 向上が，数学の UI 向上に直結する
- 数学系と情報系の人の交流が深まる
- 宣伝
論文の査読プロセスが変わる
Lean は証明アシスタントなので，
Lean で書かれた証明が正しいかどうか，コンパイルがエラーなしに通るかどうかで完璧に判定できる
ほぼすべての数学は Lean で形式化して実装することができる
という機能を持っています．したがって，論文に Lean コードを添付することが習慣化されれば，査読プロセスのうち「正しいかどうかの検証」は短時間かつ人間の手を介さずに行うことができるようになります．これにより，査読者はより本質的な検証に集中することができます．
数学を学習するのが容易になる
数学の勉強は難しいです．「形式的に定義された概念を実感としてつかむのが難しい」とか，「証明や定義のうまいアイデアを思いつくのが難しい」などいろいろな難しさがあるのですが，そのうち「証明の正しさを検証するのが大変」という難しさを，Lean は軽減してくれます．
考えてみれば，「証明の正しさを検証」するには，「いま示すべきゴール」と「いま持っている仮定」を頭の中でシミュレーションしつつ，証明の文章を１行１行追っていく必要があるわけで，大変なのは当然です．プログラムを人力で実行してエラーがでないかどうか検証するようなもの で，機械がやってくれるならそれに越したことはありません．
面倒くさい作業を Lean が肩代わりしてくれるので，学習者はより本質的なところに集中できるようになります．
おおらかに，「とりあえず動けばいいや」の精神 で数学ができるのは，数学科の学生の精神衛生上もよいのではないかと思っています．
また，数学書は書く人によって証明の丁寧さがまちまちで，本によっては「行間を読む」ことを厳しく要求されることがあります．数学を学ぶひとを大いに苦しめてきたこの現象ですが，証明を全部 Lean で書く場合は（意図的に読者への演習問題としない限り）それも起きなくなります．
数学を独学できるようになる
数学という学問は，「証明の正しさを検証する」のを自力でできるようになるまでにかなりの習熟を要するため，独学が難しい学問です．そのうえオンライン講義も少ないので，大学の数学科以外の場所で学ぶのはとても困難です．
Lean がこういう状況を変えてくれることを期待しています．Lean を使えば，証明が正しいかどうかは Lean が検証してくれます．自動採点も容易に実行できるので，オンライン講義も開催しやすくなり，Web上で無料でアクセスできる初心者向けのリソースも増えていくでしょう．さらに教材のサポートやLeanのデバッグ，Lean によるオンライン数学コンテスト等を通して，Lean を中心とした数学コミュニティが形成されていくことも期待できます．そうなれば，もっと気軽に，誰でも数学を学べるようになると思います．
実際に，早くも「数学科じゃないけどLeanで数学を学んでる」という人を私は観測しました．十分ありえる話だと思います．
数式処理システムとシームレスに連携できる
数学では計算も大事です．しかし大学で数学をやっていると登場する概念も高度化し，なかなか手計算では計算が難しいのでおろそかになりがちです．
Sage Math や Mathematica, Wolfram といったソフトを使えばかなりの部分が計算できますが，数学科で浸透しているかと言われると全然です．
なぜ浸透しないのかと言えば，紙に書かれた数学の本を読みつつ，パソコンを起動させてたまに要所の計算をちょっと実行し，また本に戻って証明を追って……という勉強スタイルがあまりにも面倒だからでしょう．最初から本全体が計算機上で実行できる形式になっていればいいのですが，証明部分はいままで自然言語で書かざるを得なかったため，それは実現できませんでした．
Lean により，より自然に数式処理システムを教材に組み込むことができるようになる可能性があります．（現時点で，Lean と数式処理システムの連携はあまり実現できていないようですが，将来的にはありえるという話です）そもそも Lean 自体がプログラミング言語 なので，簡単なアルゴリズムなら Lean で実装してそのまま動作させることができますし，「必ず有限回で終了するか」「終了までに最大で何回反復するか」といった性質も Lean でシームレスに証明できます．
Lean の UI 向上が，数学の UI 向上に直結する
Lean を使っていると「ここの定理なんて名前だったっけ？」とか「これどうやって書いたらいいんだろう」と戸惑うことがよくあります．これは Lean の学習コストを高めてしまいますが，GitHub Copilot などの生成AIと組み合わせることで軽減できると期待しています．
生成AI といえば，「間違った答えをすらすらと答えてしまう」問題があるとよく言われますが，Lean の場合は正しさの検証は Lean 側で完璧にやってくれるため，それが問題にならないのも嬉しい点です．
また，Lean はプログラミング言語でもあるので，とても拡張性が高いです．Widget を開発することにより，infoview に図形を出したり，グラフや図式を描画したりすることができます．まだまだ Lean のUIは改善される可能性があるということです．
Lean を使って数学をすることのメリットのひとつとして，この「Lean の進歩による UI 改善」のメリットを享受できることが挙げられると思います．数学科は長い間（事実ではないものの）「紙とペンだけあればできる」などと言われていたように，UI 面での改善があまりありませんでした．Lean はまだ UI 面では自然言語で証明を書くのに比べて圧倒的に快適とはいえませんが，Lean の UI には改善の余地がまだまだあるので，Lean で数学をすることで Lean を介して数学がやりやすくなる可能性があります．
現時点でも，「変数にマウスを合わせると型がわかる」とか，「補題にカーソルを合わせると主張がわかる」，「注意不足でミスを犯してもすぐにエラーとして教えてくれる」といった利点があります．
数学系と情報系の人の交流が深まる
数学は理学部であるのに対して，情報学は工学部にあります．私がいた大学だとかなり離れていて，情報系の授業を聞きに行くために頑張って歩いていた記憶があります．
これは情報と数学がかなり離れた分野だと認識されているからですが，最近ではむしろ数学と情報は（数学と物理，数学と生物などに比べて）かなり近しい分野として扱うべきではないかと思っています．
理由は，暗号理論やアルゴリズムの設計論，機械学習といった情報系の分野でかなり数学が応用されているからです．
情報系と数学科はぜひ交流を深めていくべきだと思いますし，それによって双方得られるものは大きいと思います．
Lean は，これを大いに促進する可能性があります．情報系から数学への関心は以前から大きくなっているのですが，逆方向の関心が少ないと感じていました．*1何度も言いますが Lean はそれ自体プログラミング言語 ですから，数学科のひとが Lean をきっかけに情報工学に関心を持つことはありそうですし，あってほしいと思います．
数学と情報の橋渡しとしては競技プログラミングもありますが，競技プログラミングはアルゴリズム論だけですし，基本的に証明をしません．Lean が普及した場合のインパクトはもう少し大きくなるはずです．
数学科と情報系を区別しない「数理情報学部」みたいな学部があってもいいと私は個人的に思いますが，そこまでいかなくても，交流が深まるのはいいことです．
宣伝
Leanワークショップが開催されるので今回も宣伝します！
*1:数学科の間では，就職のためにプログラミングを学ぶことはあっても，数学のためにプログラミングを学ぶことはほとんどなかったです．
