概要

Leanは数学を形式化するための プログラミング言語。 数学者が 証明や定理をコード化 し、GitHubで共有可能。 証明は tactic（戦術） と呼ばれるコマンドで構築。 不適切な公理追加で 矛盾した数学 も構築できる。 正しい公理とLeanのチェックで 信頼性ある証明 が保証される。

Leanで数学をプログラミングする体験

• Lean は主に数学者が使う 形式化言語。
• 数学の定理・証明を 構造化されたコード として記述、管理。
• 証明や定理を GitHub で共有し、他人の成果を import 可能。
• 人類の数学知識 をコードとして蓄積、検証、再利用する構想。
• コードとしての数学： 静的検証 ・ 再利用性 ・ 合成性 の確保。

Leanの基本的な証明の書き方

• 定理の例：theorem two_eq_two : 2 = 2 := by sorry

  • theorem：定理宣言
  • :：定理内容の開始
  • := by：証明開始
  • sorry：証明未完了の印

• sorryは 任意のゴールを閉じる が、実際の証明ではない。

• rflは 反射律（reflexivity） を利用し、a = a型のゴールを閉じる。

• 証明完了例：theorem two_eq_two : 2 = 2 := by rfl

• 証明済み定理は 他の証明で再利用 可能（exact two_eq_two）。

  • 例：
    • theorem two_eq_two_again : 2 = 2 := by exact two_eq_two

Leanのtactic（戦術）

• tactic とは証明を進めるためのコマンド群。
  • rfl：同値のゴールを閉じる
  • exact：既存の証明を利用
  • sorry：強制的にゴールを閉じる（非推奨）
• 証明は tacticの列 で構成され、全てのゴールを閉じる必要。

Leanで矛盾した数学を作る

• 公理（axiom）を追加することで 独自の数学体系 も構築可能。
  • 例：axiom math_is_haunted : 2 = 3
• 公理は 証明不要の事実 として扱われる。
• この公理を使えば 2 = 3 や 2 + 2 = 6 も証明可能。
• rewrite tacticで ゴールの書き換え が可能。
  • 例：rewrite [math_is_haunted]で2 + 2 = 6の証明を3 + 3 = 6に変換。
• 矛盾した公理 を入れると何でも証明できるため、 公理の選択が重要。

公理の削除と健全な数学

• 矛盾した公理を削除すると、それに依存した証明は 壊れる。
• 正しい公理体系下では、 正しい定理のみ証明可能。
• Leanは 論理的に正しい結論のみ を導けることを保証。

Leanの証明の意義と発展

• Leanは 証明チェッカー として、与えられた公理から論理的帰結のみを許容。
• tactic を駆使し、複雑な定理も分解・構成可能。
• 公理とLean自体が健全であれば、 証明も健全。
• 小さな証明から 大規模な数学的成果 まで拡張可能。

Fermat’s Last Theoremの形式化

• Fermat’s Last Theorem（フェルマーの最終定理）の形式化も進行中。
• 証明例：
  • theorem PNat.pow_add_pow_ne_pow (x y z : ℕ+) (n : ℕ) (hn : n > 2) : x^n + y^n ≠ z^n := by sorry
• 現段階ではsorryを含むが、最終的には 完全な証明 を目指す。
• 証明が完成すれば、 全てのサブ証明も正しく埋められる。

Leanを学ぶためのリソース

• Natural Numbers Game ：Leanの入門に最適なゲーム形式教材。

• Mathematics in Lean ：基礎から学べるチュートリアル。

• Tao’s Analysis Lean Companion ：Taoの解析学本のLean版。

• Lean Zulip の「new members」チャンネル：初心者歓迎のコミュニティ。

• Leanは プログラミングと数学の融合 を楽しめる新しい体験。

  • 興味が湧いたら、まずは Natural Numbers Game や Mathematics in Lean から始めると良い。