概要
Leanは数学を形式化するための プログラミング言語。 数学者が 証明や定理をコード化 し、GitHubで共有可能。 証明は tactic（戦術） と呼ばれるコマンドで構築。 不適切な公理追加で 矛盾した数学 も構築できる。 正しい公理とLeanのチェックで 信頼性ある証明 が保証される。
Leanで数学をプログラミングする体験
- Lean は主に数学者が使う 形式化言語。
- 数学の定理・証明を 構造化されたコード として記述、管理。
- 証明や定理を GitHub で共有し、他人の成果を import 可能。
- 人類の数学知識 をコードとして蓄積、検証、再利用する構想。
- コードとしての数学： 静的検証 ・ 再利用性 ・ 合成性 の確保。
Leanの基本的な証明の書き方
-
定理の例：
theorem two_eq_two : 2 = 2 := by sorrytheorem：定理宣言:：定理内容の開始:= 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 も証明可能。
rewritetacticで ゴールの書き換え が可能。- 例：
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 から始めると良い。