Lean - 数学をプログラミングする

はじめに

LLMがエンジニアに受けた理由は、LLMの不確かさをコンパイラが吸ってくれたから、というのはあるとおもいます。

他の学問にもLLMをもっと流行らせたい！特に数学でももっとAIを使いたい！となれば、コンパイラみたいなのがあればいいのでは？と思い立ちました。

実は、数学にもコンパイラがあります。 それが今回紹介するLeanです。

Leanとは

Leanは、数学の証明をプログラミング的に記述できる、定理証明支援系の一つです。

数学（特に大学数学）に慣れ親しんだ人なら、文字列を読むだけでも十分何やってるか分かるのが魅力です。

たとえば以下の問題を証明しましょう。

f(x) = x^2 が \mathbb{R}上連続であることを示せ

これを証明するLeanのコードが以下のようになります。

import Mathlib.Data.Real.Basic
import Mathlib.Topology.MetricSpace.Basic

example : Continuous (fun (x : ℝ) ↦ x ^ 2) := by
  -- 1. 位相的な連続性の定義を、距離空間の定義(ε-δ)に書き換える
  rw [Metric.continuous_iff]
  intro x₀ ε hε

  -- 2. 定数 C = 2|x₀| + 1 を置く（後の評価で使う係数）
  let C := 2 * |x₀| + 1
  have hC_pos : 0 < C := by positivity

  -- 3. δ を min(1, ε/C) と定める
  let δ := min 1 (ε / C)
  use δ

  -- 4. δ > 0 であることの証明と、ε条件の証明に分割
  constructor
  · -- δ > 0 の証明
    apply lt_min
    · norm_num
    · apply div_pos hε hC_pos

  · -- |x - x₀| < δ ⇒ |x² - x₀²| < ε の証明
    intro x h_dist
    -- 距離 dist x x₀ を |x - x₀| に書き換える
    rw [Real.dist_eq, abs_sub_comm] at h_dist
    rw [Real.dist_eq]

    -- 式変形: |x² - x₀²| = |x + x₀| * |x - x₀|
    rw [pow_two, pow_two, ← mul_self_sub_mul_self, abs_mul]

    -- 補助的な不等式の準備
    have h_delta_le_1 : δ ≤ 1 := min_le_left _ _
    have h_delta_le_eps_div_C : δ ≤ ε / C := min_le_right _ _

    -- |x + x₀| の上界を評価する
    have h_bound : |x + x₀| < C := by
      calc |x + x₀|
        _ = |(x - x₀) + 2 * x₀| := by ring_nf
        _ ≤ |x - x₀| + |2 * x₀| := abs_add _ _
        _ = |x - x₀| + 2 * |x₀| := by rw [abs_mul, abs_two]
        _ < 1 + 2 * |x₀| := by
            -- |x - x₀| < δ ≤ 1 なので |x - x₀| < 1
            have h_lt_1 : |x - x₀| < 1 := lt_of_lt_of_le h_dist h_delta_le_1
            linarith
        _ = C := by ring

    -- 結論の導出
    calc |x + x₀| * |x - x₀|
      _ < C * δ := by
          -- |x + x₀| < C かつ |x - x₀| < δ
          gcongr
          exact h_bound
          exact h_dist
      _ ≤ C * (ε / C) := by
          -- δ ≤ ε / C を代入
          gcongr
          exact h_delta_le_eps_div_C
      _ = ε := by
          -- C * (ε / C) = ε
          field_simp [hC_pos.ne']

要するに、

|x-x_0|<\delta \Rightarrow |f(x)-f(x_0)|<\varepsilon

というイプシロンデルタをやってるわけです。

Leanのコミュニティの広がり

Lean、これだけじゃなくてライブラリの発展が凄まじいです。

たとえば、冪乗関数の連続性を担保するライブラリ みたいなのがあります。要するに

f(x):x_0 \in \mathbb{R}で連続 \Rightarrow (f(x))^2:x_0 \in \mathbb{R}で連続

を担保してくれます。
これと恒等関数の連続性を組み合わせると、以下のようなLeanになります。

import Mathlib.Analysis.SpecialFunctions.Pow.Real

example : Continuous (fun (x : ℝ) ↦ x ^ 2) := by
  apply Continuous.pow
  exact continuous_id

便利！

ドキュメントも豊富に作成されています。

まとめ

Leanはめちゃ便利だし世界中の数学者によって整備されてるので、正直もっと流行って欲しい！そうすれば僕の数学のゼミがもっと楽になります。

他にもCoqとか、証明を支援する言語はたくさんあります。今後LLMの発展に伴い、それらのコミュニティがより盛り上がることを期待しています！