Theorem Proving in Lean4 を読む会#1

Theorem Proving in Lean 4 を読む会#1 2026/10/16 22:00~

今日の流れ 1. 2. 本勉強会の方針 Theorem Proving in Lean 4 を読む a. 今回は1章のみ

本勉強会の方針

本勉強会の方針 目標 ● ● ゆるくLeanに入門し、未経験の技術に触れることで知見を広める Theorem Proving in Lean 4を題材に、Leanのような定理証明支援系で証明を書 くことを体験する 進め方 ● ● ● 『Theorem Proving in Lean 4 』の要点を読む 予習・事前知識なしでもわかりやすいように解説（予定） 毎回1章進むくらいのペース で、2ヶ月程度 で読み切ることを想定

• https://leanprover.github.io/theorem_proving_in_lean4/

進め方について補足 詳しい説明は端折ります ● 詳しく知りたい場合はAIを活用して、本文を翻訳・解説させると自学自習をしやすい と思います この会の価値 ● ● 同じくLeanを学びたい人同士で疑問や質問を共有し合える Leanをこれから学ぶためのきっかけ作りにする

Theorem Proving in Lean 4 を読む

Leanの実行環境について ブラウザで動作する Lean Playground が手軽です ● おそらく、Theorem Proving in Lean 4 を読むだけならこれで完結できるはず ローカルにセットアップしたい場合は公式へ ● https://lean-lang.org/install/ ○ ● ● 公式ではVSCodeの拡張経由で入れる方法推奨とのこと VSCode拡張を経由しない場合：https://lean-lang.org/install/manual/ Dev Containerを使いたい場合は Mathlib を参考にするとよさそう ○ https://github.com/leanprover-community/mathlib4/tree/master/.devcontainer

• https://live.lean-lang.org/
• https://lean-lang.org/install/
• https://lean-lang.org/install/manual/
• https://github.com/leanprover-community/mathlib4/tree/master/.devcontainer

1. Introduction

1. Introductionの概要 定理証明系とはの説明、Leanについて、この本についての紹介の章 1.1. Computers and Theorem Proving 1.2. About Lean 1.3. About this Book 1.4. Acknowledgments

1.1. Computers and Theorem Proving 形式検証 （Formal verification） ● 論理・計算的な手法を使って、仕様を満たしていることを数学的に厳密に確かめること 対象は数学の定理だけではなく、 ● ソフトウェア ● ハードウェア ● ネットワークプロトコル ● 機械・ハイブリッドシステム なども含みます。 重要なのは、システムを数学的に記述すると、その正しさを示す作業は定理証明（Theorem proving）と 同じように扱えるという点です。逆に、数学の定理でも複雑な計算を含むなら、その計算が正しいことを検 証する必要があります。

1.1. Computers and Theorem Proving コンピュータが主張の確立を支援する方法は2つ ● 自動定理証明 （Automated theorem proving） ○ コンピュータが証明を探索 ● 対話型定理証明 （Interactive theorem proving） ○ 人間が証明を構築するのをコンピュータが支援し、最終的にその証明が正しいことを検証 Leanは自動定理証明と対話型定理証明のギャップを埋めることを目指している。 その目的は、数学的な推論と複雑なシステムについての推論の両方を支援し、どちらの領域でも主張を 検証できるようにすること。 また、Leanはプログラミング言語としても利用でき、さらにメタプログラミングを使ってLean自身の機能を 拡張することも可能。

1.3. About this Book この本は、Leanを使って証明を構築し、検証する方法 を学ぶためのもの。 まず、Leanの基礎となっている論理体系を学ぶ。 ● 依存型理論の一種 ○ より具体的には、帰納型（inductive types）を備えたCalculus of Constructionsと呼ばれる体系の一種を基礎としてい る 依存型理論を使って数学的対象を定義したり、数学的な主張を表現したりできるだけでなく、証明を書くための 言語としても利用できる。 学ぶ内容の例： ● ● ● ● ● 項の書き換え（ term rewriting） 項や式を自動的に簡約する Leanの自動化機能 elaboration（詳細化・展開） inference（型推論） Leanに固有の機能