BOOK-1 — Lean@AI — 証明先行コーディングのための次世代チュートリアル
¥2,999($19.71)
International shipping available
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協働に何をもたらすか
