公開日: 2026-08-27 / STEP: 1472 / 種類: Claude Code Skill (packaged reusable procedure)
「AI chat に 投げると 賢くなる、 役立つ部品は 作れるのか?」 という 藤本さん からの 問いに 対する、 作って動作測定する 実例。
Skill = 手順書 + Lean 4 template + worked example の パッケージ。 目標 mod class n % M = c に対して、 Collatz iteration の 決定的 K step trajectory を 分析し、 Lean 4 定理 ci K n < n を 自動的に emit する。
AI の チャットに 投げると、 賢くなる、 役立つ部品は 作れるのでしょうか?
効くタイプ: 検証器 (compile PASS/FAIL、 test suite、 数値照合) が 外から 採点できる タスクの 部品化。 モデル 重みは 変わらないが、 文脈と 手順の 型化 で 安定する。
効きにくいタイプ: 文章の 良し悪し、 着想の 面白さ (採点できないため 部品化しても 伸び幅 小)。
今回の題材 = Collatz mod-class descent。 Lean が 判定器 なので、 Skill 適用 の 前後で 「compile PASS/FAIL」 が 自動 計測できる。
.claude/skills/collatz-descent/ ├── SKILL.md # 手順 + honest scope (2.9 KB) ├── template.lean # placeholder skeleton (0.9 KB) └── example-case7d.lean # n%256=119 worked example (1.1 KB)
n = M*r + c。cs(n) を 繰り返し 適用。 各 odd step で 3*(a*r+b)+1 の v₂ を 計算。o = odd 数、 e = halving 数。 最終値 = (3^o * n + β) / 2^e。3^o ≤ 2^e が 定数余裕込みで 成立する とき、 定理を emit。 それ以外は refuse。| # | Case | Divisor chain | 期待 | Lean 実測 |
|---|---|---|---|---|
| 1 | n%256=119 (step624 既存 case7d) | /2, /2, /8 | PASS | ✅ PASS (exit 0) |
| 2 | n%256=135 (novel、 step624 未収載) | /2, /2, /4, /16 | PASS | ✅ PASS (exit 0) |
| 3 | n%256=39 (chain split、 evens 不足) | /2, /2, /4, /2 | omega REJECT | ✅ REJECT (omega could not prove) |
| 4 | n%512=39 (n%256=39 深化) | /2, /2, /4, /2, /16 | PASS | ✅ PASS (exit 0) |
4 経路 (既存再生産 / 新規生成 / 不可能拒否 / 深化 recovery) すべて 機械検証を 通過。
r=0: n=135 → 406 → 203 → 610 → 305 → 916 → 229 → 688 → /16 = 43 < 135 ✓
r=1: n=391 → 1174 → 587 → 1762 → 881 → 2644 → 661 → 1984 → /16 = 124 < 391 ✓
一般: 81r+43 < 256r+135 ⟺ 175r+92 > 0 ∀r≥0 ✓
factor: 3⁴/2⁸ = 81/256 ≈ 0.316
theorem case_256_135_lt (n : Nat) (h : n % 256 = 135) : (3*((3*((3*((3*n+1)/2)+1)/2)+1)/4)+1)/16 < n := by rw [Nat.div_lt_iff_lt_mul (by omega : 16 > 0)]; omega
Skill が やる こと: 一つの mod class に対する 代数的 descent ci K n < n のみ emit。
Skill が やらない こと:
効くタイプの 判定基準: そのタスクの 出来を 外から 採点できるか。 採点できる (Lean compile) なら 部品化で 安定、 採点できない (文章の 良し悪し) なら 効きにくい。
Lean compiler が 絶対的な 採点者 として 機能している。 Skill 自体は 「正解を 知って」 いる わけでは なく、 omega が 受理する 形に 持ち込む 手順 を 型化した だけ。 その形に できない case (n%256=39) は 自動で reject される。 この 「Skill 側の 賢さ」 と 「判定器の 厳密性」 の 分離 が 配布価値の 本質。
data/lean4-transfer/step624_COMPLETE.lean — 元 実装。 case7d_lt (n%256=119) が Skill の worked example。memory/project_step1472_collatz_descent_skill_v01_2026-08-27.md# 1. Skill を 読み込む cat .claude/skills/collatz-descent/SKILL.md # 2. novel case で 検証 (Skill を 手順書に 従って 適用) lean scratchpad/collatz_new_case_256_135.lean # PASS lean scratchpad/collatz_new_case_512_39.lean # PASS # 3. honest failure で 拒否確認 lean scratchpad/collatz_skill_negative_test.lean # exit 1 = 期待通り