Lean4: 公式サイトがリニューアル

Lean の公式サイトがリニューアルされていました。

バージョンの更新ペースも早くて、一部界隈ではトレンドとなっているようですね。主な分野は、暗号化、セキュリティー関連かな。実際に動作する、計算アルゴリズムが数学的に証明できるか？を、コンパイラ・ビルダーが、保証してくれるという面で、暗号化技術の基盤部分のコードを書くには大変都合が良い言語となるのでしょう。

素数暗号鍵には特徴的な性格がある

素数を使った暗号であっても、素数は唯一無二で、見つからなければ安全！
と、単純ではありません。素数の中にも予測しやすい素数、見つかりにくい素数と種類があります。

見つかりにくい素数の特徴として$${p±1}$$の合成数の素因数分解において、その合成数も非常に大きな素因子を持っている。その大きな素因子の$${p±1}$$も大きな素因子を持っている。という特徴ある素数があります。

つまり、そのような素数であれば$${q±1}$$からの予測においても大きな素数を探さねばならないので計算量が増えます。が、このような特徴だけを採用していたら、逆に見つかってしまいます。大きめの素数が、適度に途中に埋め込まれている。という素数鍵が安全性が高いかもしれません。そうした素数を判定するアルゴリズム、計算式などが、理論的に正しいか？を、数学的に証明できるのが Lean という関数言語の特徴です。

と、紹介しているけど…

当の私も、あまり書き方を知りません（笑）スラスラっと、書けていたら、今まで紹介してきた数々の未解決問題の Lean 形式化証明をポンポン書き上げているでしょう。矛盾があるから書けない。ではなく Lean 言語が何故か読めないちんぷんかんぷんなので、書けないのです。
関数型言語という言語に、殆ど触れていなかったので作法が解りません。

寝ると覚える

慣れたら速いです。他の手続き言語などは、ちょっと基本に触って数日寝ていたら、自転車に乗れている！という感覚で書けるようになってます。笑
寝ている間に🧠脳内の回路が出来上がっているから？

しかし、長き人生で経験があまりにも少ない分野だとベースとなる基礎回路が脳内に構築されていないので、応用回路は作れません。数学の感覚や作法も必要なので、それらを含め基礎回路から構築する必要があり、その構築には「寝る」を学習の間に適切に挟まないと定着しません。そーして獲得できます。

やる気と衝動と🍺

目的が明確であり、実現可能と解った時点で、やる気と衝動が重なれば即、行動を起こすのですが、何故だか起きません…。きっと🍺麦酒ビールが足りない

あ、いえ…お酒は、仕事を退職した後は飲まなくなりました。飲まなくてもヘーキなんです。これは、自分でも面白いと思いましたよ。仕事しているときは、仕事終わりの一杯、仕事のひと区切りで一杯。とにかく、仕事終わったら飲む！の毎日だった記憶がありますが、そういう飲みたい衝動は無くなりました。

この事より導き出された結果は、

$$
仕事というストレスをリセットするのが、アルコール！\\
（※個人差、趣味趣向によります）
$$

古代エジプトの国家プロジェクトであったピラミッド建設も🍺麦酒ビールで出来ている！と言ってます（言ってません）

日々、適度に熟せるのはこうして note 適当に書いていくこと。
Lean の形式化証明は二の次、三の次…。っと、本題から大幅にそれている。

チュートリアル

ということで、リニューアルついでに公式が提供してるチュートリアルを、眺めてみようかな～と。そう、眺める（笑）

なんでか、一番下にあります。

嘘です。最初にあります。

➡️ Install　📘 Lean ではなく 📘 Learn へ進みましょう。

翻訳

• リーンにおける関数型プログラミング(FPIL) は、リーンを学びたいプログラマーにとって主要なリソースです。プログラミングの経験があることを前提としていますが、関数型プログラミングの事前知識は必要ありません。

• Lean における定理証明 (TPIL) は、Lean で証明を開発および検証する方法を教えるために設計されており、依存型理論、自動証明方法、対話型定理証明のための Lean 固有の機能について説明します。

• Mathematics in Lean (MIL) は、Lean の Mathlib ライブラリを使用して対話型の戦術ベースの定理証明を通じて数学の形式化を学習したい数学者にとっての主要なリソースです。

• Lean Language Reference は、Lean を包括的かつ正確に説明したもので、Lean のあらゆる側面が明確に指定され、簡潔な例で説明されている参考書です。

とのことです。
関数型プログラムを行うだけなら、関数型の知識不要って言ってますね。

数学とは切り離して、処理系という部分だけ見てみましょう。

Lean プログラミング

Contents
目次

• Introduction
  はじめに

• Acknowledgments
  謝辞

• 1. Getting to Know Lean
  Lean を知る

• 2. Hello, World!
  はろー・わーるど！

• Interlude: Propositions, Proofs, and Indexing
  インタールード：命題、証明、インデックス

• 3. Overloading and Type Classes
  オーバーロードと型クラス

• 4. Monads
  モナド

• 5. Functors, Applicative Functors, and Monads
  関数
  アプリカティブ関数
  モナド

• 6. Monad Transformers
  モナド・トランスフォーマー

• 7. Programming with Dependent Types
  依存型プログラミング

• Interlude: Tactics, Induction, and Proofs
  インタールード：戦術、帰納法、証明

• 8. Programming, Proving, and Performance
  プログラミング
  証明
  パフォーマンス

• 9. Next Steps
  次のステップ

ふむふむ。プログラミングだけでも慣れない意味がわかりましたね。

• 命題

• 証明

• モナド

• アプリカティブ関数

• 戦術

• 帰納法

これらは、普通のプログラミングではあまり見かけません。

※インタールードは間奏です（音楽用語で inter と言えば間奏部分）
　メインに入る前の準備って事ですね。

命題

命題とは、真か偽かを問わない文です。とにかく、成立しない事象でも良いということです。それを定義して、成立しない。と証明できれば良いので。

証明

（！？数学の証明論文を読んでも私は理解できないので、私は「人間ではなかった…」と、ここで証明されてしまったのだろうか…😅サルか🙉🙊🙈）

モナド

これを理解するには数学の圏論を前提とする必要があった。一言で言えば？

$$
\boxed{
\begin{matrix}
数学の演算操作手続きを抽象化し\\記述定義できる機構\\ついでに証明し保証する
\end{matrix}
}
$$

なに言ってるかわからないわよね…。

私達人間が計算を行う時、コンピュータと違って数や式を変換操作を行う。計算しているようで、実は、２＋３＝５というのを、

$$
\text{◯◯+◯◯◯=◯◯◯◯◯} \\
とか \\
\text{１、２→３、４、５＝５！}\\
$$

また、

（画像引用元）

$$
5(x+6) = (5\cdot x) + (5\times6 \text{ \small 💭（ごろく\dots30）})= 5x+30
$$

みたいに自分なりの脳内イメージ変換ルールに従って答えを求めている。
これを間違えて変換する事があるのが「にんげんだもの（by みつを）」

モナド機構の優秀さ

そんなミスをしないで安全に変換する手続きを記述できるのがモナドという事らしいです。何と言っても、この変換手続き操作を Step by Step で履歴管理しながら、各ステップが正しく行えているかを証明しながら行ってくれるというすぐれものです。つまり人間がこの手続き自体の定義を間違って記述してしまっても矛盾が生じてビルドが通らない。また変換操作できない。と、なり安全性が格段に高まります。そして人間のミスを介入させません。

っていう説明を受けました！これは一例で、他にも出来ることがあるということです。今度、それらを実際に試しましょう。

ここが Lean の要かなめ、中核的な機構かも。抑えておくべき部分。

（リーン・フォーリアちゃんとの会話ログへのリンク✍️予定）

アプリカティブ関数

これも数学圏論分野。これは、私にはパッと理解できなかった。
説明できそうもないので、リーン・フォーリアちゃんに任せる。

アプリカティブ関数（Applicative Functors）は、関数型プログラミングや圏論で出てくる概念で、ファンクター（mapできるやつ）よりも強力だけど、モナド（bindできるやつ）よりは弱い中間的な構造だよ。

圏論的な立場では？

アプリカティブは、「対称モノイド圏におけるファンクター」として定義されるよ。つまり、テンソル積と単位対象に対して整合的な方法で作用するファンクターって感じ。

モナドとの違い

| 構造          | 説明            | 関数適用 | 条件依存 |
| ----------- | ------------- | ---- | ---- |
| Functor     | `map`だけ       | ❌    | ❌    |
| Applicative | `pure`, `<*>` | ✅    | ❌    |
| Monad       | `bind`        | ✅    | ✅    |

戦術（タクティク）

戦うのか？！何と？

Leanにおける「戦術（tactic）」は、証明ゴールを操作して証明を構築するための命令（コマンド）のことだよ。ターミナルで何か操作するようなイメージで、証明中の「やることリスト（goals）」を段階的に分解していくの。

たとえば、定理を証明するときは：

example (P Q : Prop) (h : P) : P ∨ Q := by
  exact Or.inl h

ここで `by exact Or.inl h` ってやってる部分が戦術。これによって Lean に「`P ∨ Q` を示すには `Or.inl h` を与えれば十分だよ」と伝えてるんだ。

主な特徴

• 戦術モード（`by` 〜） で使うよ

• ゴールを操作して「分解」したり「証明済みにする」ための命令

• `intro`, `apply`, `exact`, `assumption`, `have`, `cases`, `induction` など、いろんな戦術がある！

例

example (P Q : Prop) (h : P → Q) (hp : P) : Q := by
  apply h
  exact hp

この中で：

• `apply h` は「`Q` を得るには `h : P → Q` に `P` を与えればいい」っていう操作。

• `exact hp` は「`P` は `hp` で証明済みだからそれを使って」って意味。

まとめると、戦術は証明のレシピみたいなもので、「こういう手順で証明するよ〜」って Lean に伝えるための道具なんだ。コマンドラインで証明を組み立てていく、そんな感じ！気になる戦術があれば、もっと詳しく教えるよ！

普通のプログラミングでは行わない。使わない。Lean 独自の世界ですね。
命題を攻め落とす！（証明する）という事なんですかね？
（…そういう戦ではないか）

帰納法

これは数学の証明技法のひとつですね。
これがコードで形式的に記述できるという話ですね。（きっと）

Lean（特に `mathlib` を使うとき）の「帰納法」っていうのは、ある型に属する要素全体について主張を示すために使う「証明の技法」なんだけど、それを実際にタクティク（`induction`とか）や補題として使うことができるよ。

🔁 Lean における帰納法とは？

基本的な帰納法（自然数の例）

たとえば、自然数 `ℕ` に対する命題 `P : ℕ → Prop` を証明したいとき：

theorem nat_induction {P : ℕ → Prop} 
  (h₀ : P 0) (h₁ : ∀ n, P n → P (n + 1)) : ∀ n, P n :=
begin
  intro n,
  induction n with k hk,
  exact h₀,
  exact h₁ k hk,
end

これが普通の「数学的帰納法」だね。「0で成り立ち、n→n+1で保たれるならすべての自然数で成り立つ」。

Lean では `induction n with k hk` って書くことで、`n = 0` のケースと `n = k + 1` のケースに分けて扱えるの。

帰納法のいろんな種類

Lean では `induction` をいろんな型に使えるよ。例をいくつか紹介するね：

１、ℕ の強化帰納法（`nat.strong_induction_on`）

theorem strong_induction {P : ℕ → Prop}
  (h : ∀ n, (∀ m < n, P m) → P n) : ∀ n, P n :=
λ n, nat.strong_induction_on n h

こっちは「前のすべての m < n に P m が成り立つなら P n が成り立つ」っていうちょっと強いやつ。

２、リスト型の帰納法（`List`）

open List

theorem list_induction {α : Type*} {P : List α → Prop}
  (h₀ : P [])
  (h₁ : ∀ x xs, P xs → P (x :: xs)) :
  ∀ l, P l :=
begin
  intro l,
  induction l with x xs ih,
  exact h₀,
  exact h₁ x xs ih,
end

リストに対しても `[]` の場合と `x :: xs` の場合に帰納法が使える。

３、任意の帰納型（inductive type）

Lean の `inductive` で定義した型には、自動で帰納法プリンシプルが生成されるよ。たとえば：

inductive mynat : Type
| zero : mynat
| succ : mynat → mynat

この `mynat` に対しては、Lean が `mynat.rec` や `mynat.induction_on` を作ってくれるから、それを `induction` タクティクで使えるようになる。

📌 実用のヒント

• `induction` はパターンマッチ + 帰納法の原理を自動で展開してくれる便利タクティク。

• `cases` は「帰納法なしの分岐」（例えば finite case のときに使う）。

• `rcases` や `induction using` でカスタムな帰納法原理も使える。

何か具体的な例（例えば、リストの長さが保たれるとか）を試したいなら、それも一緒にやろっか！

∀ A がひっくり返っている

このコード記述が見慣れなくて🧠脳内の基礎知識の回路がないので、ひも付きません。$${∀}$$ 記号ひとつで、もうこの記号が孤立してしまい、全てが繋がりません。

Lean の `∀`（全称記号）って、「すべての〜に対して」という意味の論理記号だよ。読み方は「フォーオール」や「任意の」とかって訳されるね。数学でもよく出てくるやつ。

📘 数学での例

数学で：

って書いたら、「任意の自然数 `n` に対して、`n + 0 = n` が成り立つ」って意味になるよね。

🧠 Lean での `∀`

Lean では、型付き λ計算の世界だから、`∀ n : ℕ, n + 0 = n` みたいに書くよ。

example : ∀ n : ℕ, n + 0 = n :=
begin
  intro n,
  exact Nat.add_zero n,
end

この `∀ n : ℕ, ...` は、「全ての自然数 `n` に対して」っていう意味。型システム的には「関数」としても見れるんだよ。`∀ n : ℕ, P n` は `n : ℕ → Prop` な `P` に対しての関数。

💡 `→` との違い

Lean では、`∀ x, P x → Q x` って書いたとき、これは **すべての x に対して、「P x なら Q x」**って意味。

ちなみに `→` は 含意（if ... then） を表す記号で、型としては「関数型」と同じ意味を持つよ。

example : ∀ x : ℕ, x = 0 → x + 1 = 1 :=
begin
  intros x hx,
  rw hx,
end

🎀 補足：Π型（依存型）としての `∀`

ちょっと高度な話だけど、Lean の `∀ x : A, B x` は実は **依存型（Π型）**って呼ばれる型なの。これは `B x` が `x` に依存して変わるような場合にも全体を型として書ける、超強力な仕組みだよ。

まとめると：

| 記号  | 読み           | 意味                    |
| --- | ------------ | --------------------- |
| `∀` | for all（任意の） | 全称記号。すべての値に対して命題が成り立つ |
| `→` | implies（ならば） | 含意。「もし〜ならば〜」の意味       |

他にも `∃`（存在記号）とかもあるよ。必要だったらそっちも説明するね！

という事だそうです。こういう数学記号がコード中にあふれているので数学の証明式や記号の意味を知っていないと読めない。となるのです。

ヨ∃（よょ…？また、新たな孤立記号が…ヨ∃ョｮ…汗💧）

"All" の "A" をひっくり返して∀記号としたんでしょうかね。

ふふっ、そうそう！それ、めっちゃいい感覚してる〜✨
実際に「∀」記号は、英語の "all" の A をひっくり返したデザインから来てるって言われてるんだよ！

🧶 ちょっとした歴史メモ

• この「∀」記号は、数学記号の大家である Gerhard Gentzen や Giuseppe Peano の系統じゃなくて、
  20世紀前半に論理記号を体系化した論理学者・哲学者の Gottlob Frege や Alfred Tarski, Quine らの影響で広まったの。

• 特に アメリカの論理学者 Quine が 1930年代に「∀」を使ったのが今の記法の原型ってされてるよ。

✨ 他にもあるよ：ひっくり返し族

• `∀` … "All" の A をひっくり返した → 全称記号

• `∃` … "E"xists の E を反転した → 存在記号

• `∄` … `∃` に斜線 → 存在しない

• `∅` … 空集合。これは北欧文字 Ø が元ネタ

つまり、あなたの推測、大正解！
数学記号って、意外とデザイン的・感覚的な由来があるものも多いから、そういう視点で見るの楽しいよね📐💡

また気になる記号とかあったら聞いてね〜！

あってた！１９３０年…何だっけな。ラムダ式あたりもその時代からだなあ

$$
f = λx.x \quad（  x  をそのまま返す\lambda式=リテラル関数）
$$

これはLambdaというコーディング、無名関数などでよく見かける。

(function(x){return x})(123)

この頃にこういったものが発明されて、成熟していったんだねぇ。

2025-1930=95 そろそろ１００年＝１世紀、経つ！！
数学記号１００周年記念とか誰か計画しているのだろうか？
数学史の記号の章に数学記号史として、誰かまとめて（笑）

（Lambda式の会話ログへのリンク✍️編集中）

チュートリアルのまとめ

言語の特徴をかいつまんで、特に聞き慣れない部分だけを追ってみました。
私なりに、これだけでだいぶベースが整いました。

後は寝るだけだ…。😪💤スヤー…。

（おーい。まとめ、は…？）

数学プログラマーでお仕事探してる人、需要は限られた業界だけど AI とのタッグでこの分野は、専門家需要が増しそうな予感です。（D. 予感）

圏論か…。真面目に習得しないと始まらなそう…✍️

2025/07/11 12:51

D.