BOOK-1 証明先行コーディングのための次世代チュートリアル AIエージェントがLean証明を先に完成させ、そこから実装コードを導く方法論と、その原理的限界を自己再帰的メタ機構(Hooks)で押し広げる方法 Lean-driven Development for the AI Age Ken Okabe 目次 Unit 0: 証明先行という発明（招待） なぜ「型が通る」ではなく「命題が証明された」を求めるのか 本書が答える問い：AIエージェントにLean証明を書かせると、実装コードの品質は本当に上がるのか 目次 Unit 1: Curry-Howard — 証明と項の同一性 Prop as 型、proof as 項 def と theorem：カーネルでの同一性、エラボレータでの実務的差異（既定既約性） 依存型：∀の力 — なぜ普通の型システムより強い保証が持てるのか ケーススタディ：insert 関数の型 vs insert の正しさの命題 Unit 2: 証明先行ワークフロー — Lean証明 ⇒ Lean実装 テストが「試した入力」しか保証しないのに対し、証明が「ありうる入力すべて」を covering することを、3段階の難易度で具体的に体感してから、フルケーススタディへ進む。 ウォームアップ①：配列の最大値（maxOfList） 典型的なバグ：初期値を 0 に決め打ちする実装は、全要素が負の数のリストで壊れる 仕様を先に書く：∀ nums ≠ [], maxOfList nums ∈ nums ∧ ∀ x ∈ nums, x ≤ maxOfList nums 実装を証明に当てはめた瞬間、「全部負のリスト」という反例が実行前に浮かび上がる過程を追う ウォームアップ②：二分探索のオフバイワン 典型的なバグ：low := mid という更新が、探索範囲が2要素まで絞られた時点で 何も進まなくなり、無限ループに陥る（エラーも出ずフリーズする、実務で最も嫌われる型のバグ） 正しさの仕様に加え、停止性の仕様（「ループのたびに探索範囲は必ず狭くなる」）を 別途、命題として書く必要があることを示す low := mid + 1 へ直す過程で、証明が「範囲が縮む」ことを機械的に保証する ウォームアップ③：破壊的コピーのバグ 典型的なバグ：「コピーを返す」と仕様に書きながら、内部で組み込みの その場ソートメソッドを呼び、呼び出し元の元データまで書き換えてしまう 「戻り値が正しい」ことと「副作用が仕様通り存在しない」ことは別の命題であり、 後者を明示的に書かない限り証明も検証もされないことを示す フルケーススタディ：挿入ソートの正しさを証明してから実装する （Sorted・Perm を先に定義し、insert・insertionSort の正しさを証明しながら構築する） Unit 3: 層Aと層Bの区別 — なぜ万能の『正しさ判定器』は存在しないのか 「仕様が意図と一致しているか」を機械的に判定する万能手続きは存在しないことを、 Löbより先に、より基礎的な3つの定理から確立する。 層A（型検査・証明の機械的正しさ）と層B（仕様が現実の意図を正しく捉えているか）の区別 ライスの定理（Rice's Theorem）：プログラム・命題体系が持つ自明でない意味論的性質は 一般に決定不能である タルスキーの真理定義不可能性定理：ある言語で表現された文の「真理」は、 その言語自身の中では完全には定義できない（メタ言語が要る） ゲーデルの第二不完全性定理：十分強力な形式体系は自分自身の無矛盾性を 自分自身の内部だけでは証明できない この3定理は独立の根拠から同じ境界線——層Bは単一の内部的手続きでは閉じない——を 指し示していることを確認する 一段深い注記：層A（Leanカーネルの型検査）自体も、「CICという基礎理論が 無矛盾である」という前提には、ゲーデルの第二不完全性定理により、 Lean自身の内部からは証明できない残余（層Bの芯）を含む Unit 4: 登れば近づくが、経路は選べない — Löb・Turing・Feferman Unit 3が「万能ゲートの不在」を確立したのに対し、本Unitは「では自己検証を どこまで押し上げられるか」という、より踏み込んだ問いに答える。 Löbの定理（GL）の正確な定式化と証明の骨子（対角化補題・Hilbert–Bernaysの 3導出可能性条件） 「この検証で十分だ」という自己認定を、その階層自身の内部で無条件には 下せないことの、比喩ではない直接の帰結 Turingの順序数論理（1939, "Systems of Logic Based on Ordinals"）： Tₐ₊₁ = Tₐ + Con(Tₐ) として無矛盾性言明を逐次追加する超限累進 Fefermanの超限累進定理（1962）：一様反省原理を使えば、この累進は 算術の真な命題をほぼ全てカバーできる（＝希望の根拠となる肯定的な結果） しかし「次にどの方向へ登るか」という経路選択は、クリーネの順序数記法系Oの 整礎性判定がΠ¹₁完全であるために、体系の内部からは計算可能に導出できない AIエージェントの自己検証が「同一生成パス内」で完結しない理由を、 比喩ではなくここで厳密に導出する Unit 5: 天井の中で「最善」はどこにあるか 万能ゲートは存在せず（Unit 3）、自己検証にも構造的な限界がある（Unit 4）。 それでも工学的にできることは何かを、独立性という切り口から特定する。 Generator/Verifier非対称性（Debate, Irving–Christiano–Amodei 2018） — これは証明された定理ではなく設計原理であることを明示する Condorcetの陪審定理と、独立性の仮定が崩れたときに何が起きるか 同一の重みから生成された複数のサブエージェントは、なぜ独立検証者たり得ないか N-version programming の実証研究（Knight & Leveson, 1986）： 独立に書かれた実装でも、「問題そのものが本質的に難しい」箇所では相関して 同じ誤りを犯す——独立性は自動的には得られない 仕様と現実の対応は社会的プロセスでしか確立できないという指摘 （De Millo–Lipton–Perlis, "Social Processes and Proofs of Theorems and Programs", 1979） 2種類の天井の区別（本書の結論として最も重要な精密化）： 天井A（誘発の天井）：足場（後述のHooks等）は、モデルの重みにない能力を 新たに作ることはできない。ただし現状はこの天井にはまだ遠く、 独立した検証プロセスの追加によって実測可能な改善が見込める 天井B（相関の天井）：同一の重みに由来する検証はCondorcetの独立性条件を 満たさず、これは足場だけでは原理的に消せない（異種のモデル・人間など、 真に独立な情報源が必要） この区別を欠くと、「原理的限界がある」を「改善の余地がない」と過大に 読むか、逆に次のUnitで扱うHooksを万能薬だと過大に期待するか、 どちらかに振れてしまう Unit 6: 自己再帰的メタ機構 — Hooksという工学的解 本Unitの冒頭で、前提となる階層整理を明示する：Hooksは Unit 4のLöbの限界（Lean証明そのものの自己信頼の限界）を「突破する」ものではない。 Hooksが対象とするのは層Bの中でも特に、AIエージェントが生成する自然言語 （設計文書・報告）に現れる特定の修辞パターン（完了主張・必然性主張等）であり、 Leanカーネルによる証明検証（層A）とは異なるレイヤーの機構である。 この区別を曖昧にすると、教科書自身が「異なる厳密性の道具を無差別に混ぜる」 という、本書が繰り返し戒めている誤りを犯すことになる。 PreToolUse／Stopフックの仕組み（Claude Codeでの具体的な実装点） No Free Lunch定理（Wolpert–Macready, 1997）の正確な主張： 全ての可能な目的関数上の一様平均でのみ「万能に優れたアルゴリズムはない」が成立する ——「最善の固定Hook」は存在しないが、「誤りの分布」と「過検知/見逃しのコスト比」を 絞り込めば、その範囲内での最善は定義できる 汎用設計パターン（中立的な例で説明する）： regression_corpus（should_pass / should_block の両方をラベル付けした事例集。 should_pass側を欠くと、Hookは拡張するたびに過検知が増えても誰も気づけない） hook-update（新しい検知パターンを既存コーパス全件に対して回帰テストしてから コミットするゲート） fp_fn_log（実運用中の過検知／見逃しの実例を記録し、コスト比を実測し続ける仕組み） 権限分離（ラベル付けの主体と検知ロジック変更手続きの分離） よくある失敗パターンとその自己訂正の記録： 失敗①：語彙ベースの禁止リストを個別インシデントのたびに際限なく追記する 失敗②：語彙を「型」に一般化しただけで「解決した」と過大に宣言する （表現力を上げるほど検知精度が犠牲になるというNFLの警告そのものの再演） 失敗③：should_block側の事例しか持たない検知規則を設計してしまう この節はドメイン中立のテンプレートとして提示する Unit 7: 実践 — Lean@AIワークフローをプロジェクトへ組み込む CLAUDE.md / AGENTS.md への型別メタゲート組み込みテンプレート 「証明先行→実装」を新規プロジェクトで始めるためのチェックリスト よくある失敗パターンと、その型（完了主張・必然性主張・照合と導出の混同・新機構の無断導入） Unit 8: エピローグ — Lean@AI時代のコーディング体験 「証明できることしか実装しない」という規律が、AI協働に何をもたらすか

BOOK-2 関数型プログラミング入門 in Lean 4 型を通すことではなく、性質を証明しながら発見していく、AI時代の関数型プログラミング A Discovery-Driven Tutorial on Functional Programming in Lean 4 Ken Okabe 目次 Unit 0: 招待 §1 パイプライン哲学 データ変換パイプライン パイプラインのスケーリング：関数合成の技術 その他の基本的なプログラミング概念 関数型パイプラインの統一的な可能性 §2 なぜ「型が通る」だけでなく「発見しながら作る」のか 発見駆動という学び方——定義を教わるのではなく、壊れる場面から立ち上げる 二重の読者像：AIが書く／人間も書ける 前方参照を作らない、という設計方針 画像の再利用方針 §3 目次 Unit 1: 関数による構築 §1 制御フロー 構造化プログラミングの基礎：順次・選択・反復 再帰：関数型反復の基礎 §2 式 パイプラインと式（Leanの|>） 第一級関数 高階関数 §3 型とラムダ 型：スムーズなパイプラインの保証 ラムダ式（fun記法） 依存関数型 (x : α) → β x — 通常の関数型言語にはない、Lean固有の強み ジェネリック関数型：α → βの力とHOFの型分解 §4 二項演算 二項演算とパイプライン演算子 カリー化と部分適用 flipとパイプラインの再構成 §5 依存グラフ コードをどう動かすか：依存グラフによるコード駆動 ループする依存グラフと再帰の関係 純粋関数型言語という、Leanの立ち位置（IOへの予告） §6 用語と概念 関数型プログラミングの用語を、Leanのキーワードに対応づけて整理する Unit 2: 代数的構造 §1 代数的構造とパイプラインフロー §2 モノイド 結合律：堅牢な構造の構築 半群：最初の代数的構造（ゼロから自作） 単位元：演算における中立な値 モノイド：単位元を持つ半群 Lean証明：結合律・単位元則をtheoremとして実際に証明する（term-mode） §3 合成則 関数合成という自然なモノイド §4 集合論と圏論 集合論と型：深く見る 圏論の最小限の導入 §5 ファンクタ ファンクタ：関数間のマッピング（ゼロから自作） §6 モナド 世界をつなぐもう一つの橋 クライスリの矢 モナド：ゼロから自作 §7 ファンクタ／モナド則 ファンクタ則をLeanのtheoremとして証明する（term-mode） モナド則（結合律・単位元則）をtactic-modeで証明する Unit 3: 一般的なファンクタとモナド §1 恒等ファンクタ／モナド §2 Listファンクタ／モナド §3 Optionファンクタ／モナド §4 Result(Except)ファンクタ／モナド §5 IOファンクタ／モナド Unit 4: 並列計算（Applicative） §1 Two Bridges再訪とapply/map2の発見 mapをmyIDとmyApplyへ分解する HOFの持ち上げとしてのapply §2 二項演算としてのmap2 map2は二項演算をコンテナへ持ち上げる代数構造である §3 デカルト積とポイントワイズ（Zip） Listに対する2つの独立した合法な実装パターンの解剖 §4 実世界における並列処理パターン デカルト積とZip、それぞれが適する場面の実務的な使い分け §5 分類木とアプリカティブファンクターの定義 Functor・Monadと並ぶ体系としての、Applicative Functorの位置づけ §6 アプリカティブ則 Applicativeの4法則をLeanのtheoremとして実際に証明する §7 アプリカティブ則の実務的な意味 4法則が「独立性」という直感の後付けの形式化であることを見る §8 Haskellの「理論的優位性」という神話——圏論的視点からの批判的検証 Functor ⊆ Applicative ⊆ Monadという型クラス階層は圏論的必然ではなく、Haskellのエンジニアリング上の設計選択であることの検証 Listに対するデカルト積とZipという、圏論的に等しく正当な複数のApplicative構造の共存 coherenceという語の圏論的意味とPL理論的意味の違い、Lean/mathlibのdiamond問題との比較 自動解決というトレードオフの評価と、Leanが採る折衷的設計 §9 特別編：次世代のAIが学習するかもしれない話 AIの学習データが特定コミュニティの解釈に偏ることについての批判的考察 Unit 5: Timeline FRP（概念編） §1 不変の世界とFRP 不変の世界（ブロックユニバースモデル）という思想 FRPはスプレッドシートに似ている §2 コアAPIの型シグネチャと法則 map：静的な依存関係の型 bind：動的な依存関係の型 using：外部リソースとのライフサイクル同期の型 Functor/Monad則の再検証（型シグネチャと法則のみ。フルライブラリ実装はスコープ外） Unit 6: エピローグ §1 発見駆動学習が残すもの §2 特別編：AI時代のLean 4コーディング体験

BOOK-1 & 2 セット BOOK-1 証明先行コーディングのための次世代チュートリアル AIエージェントがLean証明を先に完成させ、そこから実装コードを導く方法論と、その原理的限界を自己再帰的メタ機構(Hooks)で押し広げる方法 Lean-driven Development for the AI Age BOOK-2 関数型プログラミング入門 in Lean 4 型を通すことではなく、性質を証明しながら発見していく、AI時代の関数型プログラミング A Discovery-Driven Tutorial on Functional Programming in Lean 4 Ken Okabe