Leanを学ぼう〜Leanのどキソのキソ〜

どうやら Lean がアツいらしい

そんな話を聞いたので、勉強してみることにした。 #筆者現在鋭意勉強中

初めてのLean

さて、Leanって何ぞやという人のために、ど基礎事項を書いておく。
・・・と言いながら、私も全く知らない。難しい。
Leanって名前には
＜兄貴(Coq)よりもlean(スリム)に作る＞
そんな狙いがあったとか。なかったとか。

$\underline{\text{よくわかる Lean}}$
⭐️数学の証明をコンピュータで厳密チェックする道具
定理と証明を書いたら、「一切のスキがない証明」かどうか判断してくれる。
⭐️数学専用のプログラミング言語
TeXみたいな。実際は全然違うけど、こちらがルールを覚えなきゃいけない。
⭐️巨大な数学ライブラリ(mathlib)と対話的ツール(tactics)がある
基礎的な分野はかなり網羅されてる。ありがとうございます。

そんな感じ。よーわからん。

ま、この証明が合ってるかどうか裁く、数学裁判官。そんなところだろう。
とりあえず、使わなわからんわ。

インストール

頑張って。そんなに難しくない。
今は Lean 4ってやつ。無料で使えるのも素晴らしい。
しかもVSCodeにボタン1つで導入できた。すげー。

(筆者注：Mathlibは別途インストールが必要だった。環境次第ですね
VSCodeコマンドパレットで「Project: Create Project Using Mathlib…」を選択するとサクッと作ってくれる、など、地味に関門ある？🤪)

やってみようLean

証明ってことは、定理があって、それを証明させるわけだ。
そしたら、超簡単な定理から。

初めての Lean

自然数$x$に対して、等式$x=x$が成立する。

おはよう地球🌏・・・私寝ぼけてるのかな
確かに
世界一簡単な定理と言えよう。いや、待て、証明することある！？

ないよ。$x$は$x$だもん。人間は人間だもん。みつを。
そう。数学の言葉で言うならば恒等式である。
じゃあ、恒等式はどうやって証明すればいいのかな？

theorem thm1 (x : Nat) : x = x := by rfl

これがLeanで$x=x$を証明するのに必要な言語の全て。
結果のところには「Goals accomplished!」（ゴール達成！）やったね✌️
(筆者注："Nat" は "ℕ"( \nat で入力) でも代用可。以下全て "Nat" で統一)

＜大事なポイントを3つ解説＞
1️⃣ 定理を宣言する形
theorem thm1 (x : Nat) : x = x
ここが定理を宣言する形。
「theorem thm1」は「thm1 という名前の定理を定義します」
「(x : Nat)」は「自然数$x$を1つ固定＝任意の自然数$x$について」
「: x = x」は「定理の内容＝"$x$は$x$に等しい"を伝える」
このように書くことで、こんな定理ですよ〜って言える

2️⃣ 大事な「by」
by はここから証明を書くよの合図。
これがないと、いつ証明が始まったのか。わからない。💦
でも...
特例があって、「式が1つの時は by はなくてもいい」ってのがある（今回も⭕️）
まぁでも、大事な by。

3️⃣ rfl は『左辺と右辺が全く同じだから自動で証明できるよ』のコマンド
今回は$x=x$で、左辺と右辺が「全く同じ式」だから、これでOK。
ちなみに rfl は reflective (反射律) ですね。同値関係で出てくる概念。

・・・ここまでは Hello World! 程度のものと思えば。 #おはよう地球

（筆者注：1行目に「Import Mathlib」と書くことが大事です、端折ってます笑）

Mathlib えらい

さて、お次は何がくるのかな？？

高校生が苦しむアレ

$\sqrt{2}$は無理数である。

キタよこれ😮‍💨
概略だけでも。復習のために。えーっと、どうするんだっけ

(概略)

$\sqrt{2}$が有理数だと仮定して、$\sqrt{2}=p/q$とおく。($p, q$は互いに素な整数)
整理すると$p^2=2q^2$になる。
$p$が奇数なら偶奇が違うのでおかしい。$p$は偶数で、$p=2r$とする。($r$は整数)
整理すると$q^2=2r^2$になり、同様に$q$も偶数がわかる。
以上より$p, q$は両方偶数となるが、これは$p, q$が互いに素であることに反し矛盾。
ゆえに$\sqrt{2}$は無理数である。

だいぶ込み入ってきてるなぁ...
これは、どうやってLeanで証明を表現すればいいのかな。

theorem thm2 : Irrational (Real.sqrt 2) := by
　simpa using irrational_sqrt_two

え？？？終わり？？？
うん。これで証明は終わりである。
すなわち、Mathlibには予め$\sqrt{2}$は無理数だという定理が入っているのだ。
ありがとう神様👼

なるほど、Leanに予め入っている定理の呼び出し方を知る、ということね。
で、今回も注目ポイントは...3つ！

＜大事なポイントを3つ解説＞
⓵ 形が違っても「Irrational (Real.sqrt 2)」は定理（命題）になる！
「$x=x$」と同じ。それだけで「真」か「偽」か決まるのが大事。
⓶「irrational_sqrt_two」は既にMathlibで証明されている定理
⓷「simpa using」は「その証明をそのままゴールに当てはめる」もの
正確に言うと「simpa」は「ちょっとだけ書き換えとかを含む」けど、これはそのうちまたわかるさ。

なるほど。基本的な意図は伝わったかな😔
「$\sqrt{2}$は無理数である」という命題を示すために
「$\sqrt{2}$は無理数である」という定理を引っ張ってきた感じ。

Leanの裏ジジョウ

自乗(2乗)だけに...🤣

さて
私は最初にこう書いた。

定理と証明を書いたら、「一切のスキがない証明」かどうか判断してくれる

ってね。でさ、今の「$\sqrt{2}$は無理数である」の証明には、スキがないのかな？
Lean的に(Mathlib的に)納得してるからOK。
みたいにはしたくないので、ちょっとここから裏事情をお話しするタイム。
ただし
別に全部の裏背景を語るつもりもない。必要に追われたから💦💦
というか・・・

世の中のLeanの本/記事は、このパートが非常に長くて初学者を苦しめる。

最初からテレビ📺の全ての機能を知らなくても、観れればいいでしょ。最初は。
でもテレビの仕組みは複雑なのよ。
そんなもんさ。

Mathlibの中には何が書いてあるの？

結論から言おう。
Mathlibとは、「Leanの言葉で書かれた巨大な数学ノート」だ。
その中には、たくさんの定義・定理・証明が載っている。

何個あるの？？って感じ。
もちろん、世の中の数学の定理全部、には程遠い。逆に重くなっちゃう🪨
高校の時に「定理集の虎の巻」とかもらったことあったが、あれに近いかも。

もちろん、irrational_sqrt_two も「名前のついた一つの定理」で
その証明も含めてMathlibには書かれている。
だから安心なのだ。
「これここの定理の話や！解ける！以上」みたいな。
カンニング...とは遠からず近からず、「持ち込みOKテスト」が近いかも？

さてさて
数学の定理って積み上げ式だ。
さっきの「$\sqrt{2}$は無理数である」の証明も
その中に「$p^2$が偶数ならば$p$は偶数」という定理を使ってて、みたいな。
そんなものよね。
毎回毎回「1の次を2と言います」から始めてたら辛いよ😞
だから
Mathlibの定理の中にある証明も、また別のMathlibの定理を中で使って示している、みたいな入れ子構造が半端ない。
「50ページを読んでたけど、ここを知るためには47ページと49ページが必要で、47ページを知るには5ページと31ページと...」
あぁ。数学者ってこういう気分になるのよ。この理論遡り絶望感。
でも大丈夫。
Mathlibに書かれていることは「全て正しい」から。
安心して遡ることなく使っていい。

irrational_sqrt_twoって何者？（注：長すぎるので編集する説）

Mathlibは無料で見れる。ソースが。醤油じゃねぇぞ。ソースコード。
だから、
「irrational_sqrt_twoがどう定義されてどう証明されたか」も全部追える。
世界中常に毎秒晒されていると思えば、信ぴょう性は上がると思う。

ちなみに見ておくと、こんなことが書いてある。

/-- Irrationality of the Square Root of 2 -/
theorem irrational_sqrt_two : Irrational (√2) := by
　simpa using Nat.prime_two.irrational_sqrt

（筆者注：√2は Real.sqrt 2 と同じ）

またsimpa usingの登場だ。ってか、え？これだけ？
えぇ。これだけだ。大元が。
「証明の本丸＝simpa usingの後ろ」だけを簡単に解説しておくと...

サクッと全ての説明をするのは現状無理がありますが
もちろん伏線回収は前提として言うと...

「Nat.prime_two.irrational_sqrt」は2つの定理が合体している形。
具体的には
「Nat.prime_two」＝「2は素数である」という定理と
「Nat.Prime.irrational_sqrt」＝「素数$p$に対して$\sqrt{p}$は無理数である」という定理とが合体しているのだ。

ガンダムの合体みたいなものと思ってもいいかもしれない。
あるいはポケモンのわざみたいな✨
上の定理は具体的な素数性の主張で、
下の定理は素数$p$に対して使える「わざマシン」かもしれない。
じゃあ「Nat.Prime.irrational_sqrt」には何が書いてあるの？ってのをやると理論の遡り絶望が始まってしまうので、気になる時に調べたらいい。

いずれにせよ、
元の「irrational_sqrt_two」の証明がこれで終わっていることになる。
Irrational (√2) := by のあとに、この合体証明が書かれていただけ。

theorem irrational_sqrt_two : Irrational (√2) := by
　simpa using Nat.prime_two.irrational_sqrt

忘れた頃に改めて。
じゃあ、「x = x」とか「Irrational (√2)」とか
そもそも命題って何だろう？

命題って、その文章から「真」か「偽」か判定できうるもの。
（未解決問題のように「知らないです...人類が...」というものも含む）
「x = x」はわかるけど「Irrational (√2)」って何？？
って人のために補足しておくと
この「Irrational」ってのが便利でさ。
「Irrational x」とか書くと、「実数 x は無理数です」っていう意味の命題。
だから数学の言葉で言うなら「実数から命題への写像」ってところかな。
ただただ「$\sqrt{2}$は無理数です」って言ってただけ。

ふと思ったのは、閻魔大王👹の審判みたいなものかもしれない。
(天国地獄の二分だけってことだけに絞らせていただく💦)
命題は、その人が現世に行った罪を述べること。
閻魔大王は「天国に行くべき人を地獄に行かせてはいけない」ので
正確に判断する必要がある。
だから、「3は大きい数です」みたいな主張は許されないのだ。
「あの日あの瞬間あの場所で、あの人からあの金品を奪いました」と正確に述べなければならない。

(YouTubeの期間限定公開で鬼灯の冷徹を見て、地獄〜地獄〜ってなってたマン)
閻魔大王がちゃんとしないと鬼灯くんに怒られちゃうし。

で、それでちゃんと吐かせた罪＝命題に対して、
証拠を見ながら天国か地獄か判断するわけだ。
その時に
閻魔様はいちいち公理系からやってたら時間かかるし、使える過去の判例は手札にあっていつでも使えるようにしておく、ってわけ。

まとめるなら、
irrational_sqrt_two というmathlibの定理は、
「Irrational (Real.sqrt 2)」という命題の真偽を与えるまでの
証拠の一連の使い方が書いてある、とも言える。
だから

theorem thm2 : Irrational (Real.sqrt 2) := by
　simpa using irrational_sqrt_two

「Irrational (Real.sqrt 2)」は「irrational_sqrt_two」と同じ「型」を持っているからこれで示せるね👹
という半ばトートロジー的な証明ができていたことになる。

Lean で言う「型」って何？

さて、これをどこまで真面目に語るのかですが...
私が「型理論」を深く知ってるわけないやん💦

データって色々あると思うんだよね。
「罪状総括」「具体的な行為」「主語となる人」「その時の天気」・・・
閻魔様の前にはカードがいっぱい散らばっていて、組み立てなきゃいけない。
その時に
「罪状総括は黒色」「具体的行為は白色」「人は黄色」「天気は緑色」・・・
みたいな、ラベルをつけておけば、閻魔様も整理しやすいと思うんだよね。

Leanで言う「型」は（一般的に言われる「データ型」は）この色ラベルだと思ってくれればいい。とりあえず。

「3」という自然数には「自然数＝Nat」という型をつけよう
・・・だから定理1で「(x: Nat)」って書いてた
「2.5」という実数には「実数＝Real」という型をつけよう
とかすれば
「3+"Hello!"」みたいな変な文章って避けられるよね

まぁこの辺は簡単だけど
ここからちょっとややこしい！！

「Irrational (Real.sqrt 2)」という命題には
もちろんそれ自身には「命題＝Prop」という型がついてる。
それは事実。
が。
「$\sqrt{2}$が無理数である」という証明は、1通りじゃないと思う。
何を先に仮定するか、とか、そもそもかなり違って見える証明だってある。
（$x^2-2=0$の解と見て、有理数ならば分母が最高次係数1の約数になって整数になるけどそんな整数はない、とかでもいい）
この「$\sqrt{2}$が無理数である」に至る証明それぞれに対し
「Irrational (Real.sqrt 2)」という名前の型を当てる
これがちょっとややこしく見えるところだ。

命題にはProp型というラベルがついてるが、
それと同時に、個々の命題は証明の型のラベル名なのだ。

このように見ると、
命題は「証明の型(ラベル)」になり、証明はその型の値になる
これがいわゆる
Curry–Howard 対応（命題＝型、証明＝項）である。
Lean は、
書かれた式が本当にその命題の型を持っているかどうか
（＝正しい証明になっているかどうか）
を型チェックとして機械的に確認している。

だから
irrational_sqrt_twoでは