この記事は定理証明支援系 Advent Calendar 2023 の参加記事です．
お誘いくださった Palalansoukîさん ありがとうございました．
はじめに
私は最近 Lean4 というプログラミング言語兼定理証明支援系の勉強がマイブームなので，それについてお話していきたいと思います．
Lean4，ご存じでしょうか？Lean という言語自体は 2013 年ごろから開発が始められているそうですが，バージョン 4 の公式リリースが出たのはつい最近で，なんと今年の9月8日です．
そして Lean4 は 3 以前とは互換性がないので，実質的に新しい言語であると言っても過言ではなく，つまりは「最近リリースされたばかり」というわけです．読者の方がご存じないとしても，無理もないですね．
まだ新しく，ライブラリが充実していないため不便で，数年は求人が発生することもなさそう*1な言語ですが，なかなかおもしろい言語なんですよ．
証明の検証ができる
まず，Lean4 は「定理証明支援系」として使うことができます．つまりは，証明をコードとして表現し，検証することができます．具体的には，Lean で書かれた証明はコンパイルが通れば正しく*2，コンパイルが通らなければどこかで間違っているという性質を持ちます．
「証明」という言葉からイメージされるように数学の定理を検証することができるほか，アルゴリズムが意図した解を返すことを（テストではなく！）証明することだってできます．安全性をすごく重視した言語だと思っていただければ良いかもしれません．
どうやったらそんなことができるのか不思議に思われるかもしれません．複数の戦略がありえるようですが，Lean4 の場合，型理論をうまく使っています．
型というとたとえば Python であれば文字列とか Bool 値とかがあるわけですが，Lean の場合には Prop という型が用意されています．Prop というのは命題 (proposition) を意味しており，文字通り 1 + 1 = 2 のような命題が Prop 型を持ちます．そして，ここが大事な点ですが， 1 + 1 = 2 という命題自身が型になっています．
命題が型ということは，項を持つかもしれないということです．命題の項は証明として機能し，ある命題 P を証明するということは，Lean では型 P を持つ項 h : P を構成することに言い換えられます．
要するに，型システムを通して「命題を証明する」という数学の話が「証明項を構成する」というプログラムの話に置き換えられるわけです．
数学の理論が表現できる
証明が検証できるというだけでもおもしろいと思いますが，今までの話には少し抜け穴がありました．
Lean で書かれた証明はコンパイルが通れば正しく，コンパイルが通らなければどこかで間違っている
ここの表現ですが，「数学の理論を Lean で表現することができる」とは書かなかったことにお気づきでしょうか？実際いくら証明を検証するのが容易でも，命題を形式化するのが不可能または困難であれば困ってしまうわけですが，Lean の場合これも高い水準でクリアしています．
mathlib4 という大学レベルの数学の多くの部分を含むライブラリが開発されているほか，Liquid Tensor Experiment といって実際に数学の論文を形式化した例もあります．これは Peter Scholze というフィールズ賞を受賞した数学者からの，この論文を Lean で形式化してみてくれという挑戦を受けて立ったものでした．(LTE は Lean4 ではなく Lean3 で行われました)
leanprover-community.github.io
また，2023 年現在始まっていませんが，Lean4 でフェルマーの最終定理を形式化しようという計画 *3 もあります．
通常数学は公理的集合論というもので基礎付けられるのに対して，前述のように Lean は型理論に基礎があります．集合論と型理論の違いはそれなりに大きく，両者の翻訳が常にできるという保証があるわけではないようです．しかし上記のような実績が示すように，Lean のような定理証明支援系は普通の数学を形式化する能力があると思って問題ありません．
数学フレンドリーな表記法
このように，Lean は数学の理論を形式化し，検証する能力があるというお話をしてきましたが，しかしプログラミング言語であるわけです．想定される主なユーザ層には数学科の学生や教員が含まれているわけですが，そういった層がプログラミングに慣れているとは限りません．そういう方でもスムーズに学習できるような仕様になっているのだろうかということが当然気になってきます．
特に，コードが読めるのかどうかが問題ですね．
いくら Lean が数学の証明の検証を自動的にやってくれるとはいっても，「書かれているコードが表すものと，示したい定理が一致していること」の検証はやはり人間がせざるをえないわけです．だとすれば，コードが数学の文章として読みやすいものかどうかは重要な問題です．
Lean がこの問題に対して対応した手段の一つは，Unicode を使って数学記号を表現することでした．VSCode などのエディタ上で（適切な拡張機能を入れたうえで） \ などの記号を入力すると Unicode 入力モードになり，かなりの数学記号が入力できます．たとえば \a と打つことで α が入力出来ますし，\to と打てば → が入力できます．
通常の数学文書では $ 記号でマークアップする記法で数学記号を出力する， LaTeX と呼ばれるツールが使われることをご存じかもしれません．Lean の Unicode 入力は LaTeX に対応するものですが，証明の形式化という視点からは LaTeX よりずっと便利なものです．より高速に入力できますし，画像などではなくてあくまで文字なので，コピーなど機械で処理するのにずっと都合がよいのです．
証明の自動化ができる
ところで，数学を Lean に検証させるということは「機械でもわかるように」丁寧に証明を書かなくてはいけないということです．機械は人間に比べてどうしても融通が利きませんが，証明を書くのが面倒になってしまわないのでしょうか．
これにてついては，正直に言って，多少面倒になりはします．しかしそれは完璧にフォーマルで機械可読な証明を書くという要件からくるもので，Lean という言語の性能が悪いからではありません．Lean はむしろ，普通に書くと面倒になってしまう証明を自動化して楽にする方法をいくつも提供してくれています．
その最たるものがタクティクです．証明をするとは，Lean では「与えられた型を持つ証明項を構成する」ということです．それを直接関数適用やラムダ式で実行することもできるのですが，タクティクを使って構成するという選択肢が用意されています．
たとえば simp というタクティクは，ゴール（現在示すべきこと）をあらかじめ登録したルールをもとに自動で簡略化してくれます．例を挙げると a + 0 = a のようなルールは @[simp] アトリビュートがつけられて事前に登録してあるため，毎度「このルールを使って……」と明示的に指定せずとも適用されます．便利ですよ．
この記事ではコード例を出さない方針ですので，ここで詳細については書きません．Lean のタクティクについては「タクティク逆引きリスト」を作成したので，詳しく知りたい方はそちらをご覧ください．
また，生成 AI との組み合わせも最近よく研究されています．最近だと morph-prover というのが出ていますね．
既存ツールでも，GitHub Copilot はありがちな証明を自動で補完してくれたりと，結構サポートしてくれます．
自然言語で証明を書いている場合は，機械が提案した証明が正しいのか検証するコストがメリットを上回ってしまうため使えそうにありませんが，Lean では検証コストが低いので活用が積極的に行われています．
関数型プログラミングの考え方が学べる
ここまで数学の形式化という視点から話をしてきましたが，そもそも Lean はプログラミング言語なのでした．パラダイムとしては，純粋で正格評価の関数型言語です．そういう意味では Haskell に似ています．
Haskell という言語は，プログラミング言語の中でもちょっと立ち位置が特殊であるようですね．開発のために学ぶというより，関数型という考え方を学ぶために，あるいは数学的なバックグラウンドに興味があって，という目的で学ぶ人がいるようです．関数型プログラミングを勉強したいなら，Haskell をやるのがいいという意見を何度か聞いたことがあります．
Lean は，ここに新たな風を吹き込むことができるかもしれません．
実際 Lean は比較的後発の言語だけあって，Haskell よりもモダンな設計になっています．#eval で即座に実行することができたり，#guard で手軽にテストができたり，#find でライブラリ検索ができたりするのは明確に利点でしょう．パターンマッチングもより簡潔に書けますし，Haskell の売りの一つである型の表現力も Lean の方が高く，そして再帰関数がうっかり無限ループしてしまうバグも Lean なら起こりません．*4 かつ，コードの理解を難しくし，デバッグをやりづらくする遅延評価がないので関数型プログラミングというパラダイムの理解に集中できます．
「数理的側面に興味がある」から関数型プログラミングを学びたいというなら, ますます Lean は好適であるはずです．
おわりに
数学やプログラミングの予備知識を特に仮定せず，ここまで Lean Prover の何がおもしろいのか，どうして学ぶべきなのかというお話をしてきました．
Lean を学ぶことで，プログラミングに既に親しまれている方なら考え方の幅が広がるかもしれませんし，数学に興味がある方ならソフトウェアとして数学理論を実装するという体験から新しい知見が得られるかもしれません．
興味を持っていただけたなら幸いです．読んでいただきありがとうございました．
*1:海外ではすでに求人があるようですが，日本ではしばらくないと思います
*2:sorryAx を使っていないという前提条件は必要ですが，意図的に話を簡略化しています
*3:https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/Formalising.20Fermat
*4: Lean では，再帰関数を定義したら有限回の呼び出しで停止することを証明しないとエラーになってしまいます．partial と明確にマークしない限り，証明なしでは実行できません
