数学は幽霊がいる

• Leanは数学を形式化できるよう設計されたプログラミング言語で、数学者が数学の定理をコードのように扱えるようにする
• 利用者は定理、証明、公理などをコードの形で作成し、証明過程は tactic と呼ばれる命令セットを通じて進められる
• 証明が実際に完成していなくても sorry で一時的に差し止めることができるが、これはTypeScriptのanyに似た偽証明である
• 公理を誤って追加すると（例: 2 = 3）、論理的矛盾とすべての命題の証明可能性という危険が生じる
• Leanは論理的に選択した公理と証明体系の上でのみ結論を導くため、数学的妥当性を維持することが重要な意味を持つ

---

Lean: 数学をコードで扱う言語

• Leanは、形式化された数学を記述するために特化したプログラミング言語である
• 数学者はLeanを通じて数学をコードとして表現し、互いの定理と証明を構造化することで協働と共有を可能にする
• 未来的には、人類の膨大な数学知識がコードの形で機械的に検証・組み合わせ可能になる未来を提示している

Lean証明の第一歩

• theorem two_eq_two : 2 = 2 := by sorry の形式で、Leanでは簡単な定理宣言が可能
• 証明が未完成のときは sorry を入れるが、これは一時しのぎにすぎず実際の証明ではない
  • sorry はLeanの証明検証を通過させるが、論理的には信頼できない
• 完全な証明を行うには、rfl（reflexivity）などの tactic を使って、2 = 2 のような自明な等式を証明する
• 既に証明済みの内容は、exact などを使って他の定理で再利用できるため、モジュール性を重視できる

公理と矛盾：数学が“幽霊”に取り憑かれたとき

• もし axiom math_is_haunted : 2 = 3 のような公理を追加すると、Leanはそれを真実として扱う
• この公理は後の証明過程で利用可能となり、数学的に成立しない結論（例: 2 + 2 = 6）までも証明可能になる
• rewrite tacticを使って 2 を 3 に置換し、rfl で等式証明手続きを完了することができる
• 不適切な公理によって矛盾が導入されると、Leanでもすべての命題が証明可能な状態（論理的崩壊）が発生する
• 実際、20世紀初頭にはラッセルのパラドックスなど、公理系内の矛盾が数学の根本的な考察へとつながった
• このように、公理の選択が論理体系の妥当性維持に決定的であることを、Leanはよく示している

証明検証器（proof checker）としてのLean

• 公理が適切に選ばれ、Leanが論理的に正しければ、理論的に信頼できる結論を提示する
• 単純な等式から非常に複雑な定理（例: Fermatの最終定理）まで同じ原理で検証される
• 大規模な定理は、下位構造と定理の反復的な証明積み上げによって全体のツリーが完成する構造である
• 例として、Fermat's Last Theorem（フェルマーの最終定理）をLeanで形式化する大規模プロジェクトが進行中で、最終的には暫定証明（sorry）なしの正式な証明体系が完成する予定だ

Leanを学ぶ楽しさ

• Leanによる証明はコーディングと数学の創造的な融合である
• 始めは簡単な命題を証明する方法から、次第に複雑で深い数学を厳密に積み上げる過程が重要な楽しみとなる
• 公式チュートリアルやコミュニティ資料（例: Natural Numbers Game、Mathematics in Lean など）が、入門に適している
• Leanを使うと、直接ロジックを形式化しながら、巧妙なアイデアと議論の美しさを再発見できる
• 根拠がない場合でも、ある種の人々にとってはLeanが特別な楽しさをもたらすという結論で締めくくられている