STEP 1351 / 1360v0.3 EDUCATION KIT + POE v0.1 (STEP 1305) 概念 demonstrator → v0.2 (STEP 1351) 3 層構造 → v0.3 (STEP 1360) 予測記入 zone + 匿名 counter (STEP 番号 collision 訂正 5 例目: 初稿 1359 → 別 tab で 同時進行の rei-preregister spike が 先取り → 1360 renumber、 SAC-4 事後訂正)

Collatz Learning Kit — 触って見る 未解決問題

Silent Visual Verifier Collatz-track v0.3 = v0.2 (3 層教材) + POE 予測記入 zone (押す前に 予測を 書くと 外れの 瞬間が 学びに 変わる)。 v0.3 追加起点 = chat-Claude 2026-08-21 turn 「動くものを 見ると 分かった気に なるが、 それは 理解ではなく 納得。 学習に 変わるのは 一手加えた時だけ」 + STEP 1358 Statistics 教材 v0.2 で 同型 template 確立、 本 STEP は Collatz domain 移植。 上層 (小中高生): 触って見る Collatz orbit + t₁=1 下降エンジン + 予測記入 / 中層 (教員): 5 分で 授業に組み込める drop-in + POE 予測活動 + Discussion prompts / 下層 (研究者・院生): STEP 614-624 Lean 4 axiom-free 48 定理 + trailing ones 79% 壁 empirical + Chang 20/29 + Paper 145 v0.9-c DOI。 単一 HTML、 login 不要、 install 不要、 リンク一つで 授業に組み込める。 藤本伸樹 × Claude Code / 2026-08-20 → 08-21 v0.3

student1. Collatz 予想 とは (1 分で 分かる)

ルール は 二つだけ:

  1. 偶数なら 半分に する (n → n/2)
  2. 奇数なら 3 倍して 1 足す (n → 3n+1)

これを 繰り返すと、 どんな 正の整数 から 始めても、 いつか 1 に 到達する? が Collatz 予想 (角谷の問題)。 1937 年に Lothar Collatz が 出題、 90 年近く 誰も 証明できていない。 コンピュータで n = 2⁶⁸ (約 3×10²⁰) まで 全部 確認済み、 反例は 一つも 見つかっていない、 だが 「全ての n」 の 保証は まだ。

Paul Erdős は 「数学は この問題に まだ 準備が できていない」 と 述べた。

student2. 触ってみる

数を 入れて 「verify」 を 押すと、 その 数から 始まる orbit (道筋) が グラフ化される。 色分け は、 各 step で 何が 起きているか を示す (詳細は 次の 「下降エンジン」 で 説明)。

preset: 1 (base) 2 (1 step) 3 7 12 27 (famous) 31 127 703 6171 77031

verify を 押す前に 予想を 書いてみてください (空欄可、 記入時のみ 予測 vs 実測 差分を 表示)。 「予測が 外れる」 瞬間が Collatz orbit の 直観外れさを 掴む 一番の 学び。

t₁=0 (偶数、 単純に半分) t₁=1 (下降エンジン、 Case 1) t₁=2 (Case 2 証明済) t₁=3 (Case 3-4 証明済) t₁≥4 (Cases 5-8 未解決の 壁)

student3. 下降エンジン t₁=1 (Rei 独自の見せどころ)

t₁ (trailing 1-bits) = 奇数を 2 進数で 書いたとき、 末尾に 1 が 何個 連続で 並んでいるか:

  • 3 = 11₂ → t₁=2
  • 5 = 101₂ → t₁=1
  • 7 = 111₂ → t₁=3
  • 27 = 11011₂ → t₁=2
  • 127 = 1111111₂ → t₁=7 (壁)

t₁=1 の 奇数は、 3n+1 → /2 → /2 で 必ず 元の数より 小さくなる (2 回で 平均 3/4 倍)。 これが 「下降エンジン」。 Rei の Lean 4 axiom-free 証明 (STEP 622-624) は この t₁ が 小さい範囲で 全 orbit が 1 に 到達することを 機械検証済み。

逆に t₁ が 大きい 奇数は、 3n+1 で 一気に 大きくなる 可能性 が ある (t₁=7 の n=127 で 実際に 大きく振動)。 これが 「壁」。 t₁ ≥ 4 の 領域は、 経験的には (2⁶⁸ まで) 全 orbit が 1 に 到達するが、 Rei の 現時点の formal 証明の 外側 = 「わからない」 と 正直に 返す。

teacher4. 5 分で 授業に組み込める drop-in

学習目標 (どの科目・学年でも 転用可能)

  • 「未解決」 を 扱う 姿勢: 全部 分かる ことが 数学ではない、 90 年 分からない 問題が 現在進行形で 存在する
  • 「知らない」 と 「無い」 の 区別: 反例が 「見つかっていない」 と 「無い」 は 違う (empirical vs proven の 区別)
  • 数の 構造の 手触り: 2 進数表現 が 挙動を 支配する (t₁ の 大小が descent を 決める)

授業活動 3 例 (学年別)

小中高 (触って驚く、 5 分) — v0.3 POE 版 推奨

  1. 予測 zone に 書かせる 順序: 生徒に n = 27 を 入力させ、 verify を 押す前 に 「停止時間 予測 (何 step?)」 「orbit 最大値 予測」 「D-FUMT₈ verdict 予測 (TRUE / NEITHER)」 を 書かせる (30-60 秒)。 多くの 生徒は 「10-20 step くらい?」 「最大 100 くらい?」 「有名だから TRUE?」 と 過小予測する。
  2. verify を 押す → 実測 111 step、 最大 9232、 verdict = NEITHER (途中で n=31 = 11111₂、 t₁=5 の 壁 を 経由するため)。 予測 vs 実測 pane で 差分が 表示される。 「10 vs 111」 「100 vs 9232」 「TRUE vs NEITHER」 の 三重 桁ちがい が 学びの 瞬間 (POE Predict-Observe-Explain の 実装)。 「有名な 27 が 実は 壁越え」 は 教材の 見せどころ。
  3. 「なぜ n=27 だけ こんなに かかるのか?」 を 議論 (2 進数 11011 の t₁=2、 加えて 途中で 出てくる 数の t₁ が 高い)、 preset を 順に 触る → color pattern (緑・黄・赤) の 頻度が 数によって 違うことを 見せる。

高校・大学 (2 進数と descent、 10 分)

  1. t₁ の 定義を 板書 (末尾 1-bits)、 手計算で n=3/5/7/15/31 の t₁ を 求める
  2. t₁=1 のとき 3n+1 の 挙動を 手計算: 例えば n=5 → 16 → 8 → 4 → 2 → 1 (5 → /2 → /2 → /2 → 1、 5 step で 1)
  3. t₁ が 大きい 例 (n=127) を verify → 「なぜ 壁 なのか」 を 議論、 empirical vs proof の 違いを 導入

院生・研究者 (Lean 4 に触る、 20 分)

  1. 下記 「研究者層」 の Lean 4 code snippet を 表示、 Cases 1-4 の zero-sorry proof を 追う
  2. Cases 5-8 の open 部分 (batch_10000 + strong_ind) を 議論、 「なぜ mod 分析が 有限にならないか」
  3. 各自 Zenodo DOI から Paper 55 (STEP 614-624 origin) を dl して 精読

Discussion prompts (どの学年でも)

Q1. n=1 の verdict は 「ZERO (〇)」 になる。 なぜ TRUE ではないのか? (答え: 「vacuous」 = 何も 起きていない、 base case で 「証明」 の 対象ですらない。 D-FUMT₈ の 「未問」 と 対応)
Q2. n=6 の verdict は TRUE (下降完全)、 n=7 は? verify して 比較。 (答え: n=7 は 16 step、 t₁=3 が 出るが 4 未満 なので TRUE 継続)
Q3. 反例が 見つかったら 数学界に 何が 起きるか? (empirical で 2⁶⁸ まで 検証済 の 意味を 議論、 「実験で 見つからない」 と 「存在しない」 の gap)
Q4. NEITHER (わからない) と 答える 検証器 の 価値は? (通常の verifier は TRUE/FALSE の 2 値、 「わからない」 を 隠す。 未解決問題を 教える時 に 「わからない」 を 第一級で 返せる 教材の 意義)
Q5 (v0.3 POE 版). n=703 を 予測 zone に 「TRUE (下降完全)」 と 書いて verify すると、 実測 verdict = NEITHER (t₁≥4 の 壁 に 触れる)。 予測 外れの 瞬間に 何を 議論すべきか? (答え: 「t₁≥4 zone は 経験的 (2⁶⁸ まで) には 全 orbit が 1 に 到達するが、 Rei の formal 証明の 外側 = わからない と 正直に 返す 領域」。 二値判定なら 「TRUE (経験的)」 と 誤導、 NEITHER は 「証明済 vs 経験的」 gap を 明示。 これが 未解決問題を 教える 教材の 核。)

準備物 (0)

本 page 一つ、 URL を 板書 or QR コードで 配布、 login 不要、 install 不要、 スマホ / タブレット / PC 全対応。 授業前 5 分で 動作確認 (preset を 3 個 触るだけ)。

researcher5. 研究者・院生 向け 深層

STEP 614-624 — Collatz zero-sorry 48 定理 (Lean 4 axiom-free)

Rei-AIOS Collatz 証明 チェーン、 2026-05 頃 STEP 622-624 で 完成:

file定理数内容
step614_unified_theorem.lean7THE_THEOREM: ∀ k ≥ 2, ∀ q (odd), trailingOnes 下降
step622_exhaustive.lean15exhaustive (8 ケース) + descent_all (∀ n ≥ 12) + base cases
step623_v3.lean8Cases 1-4: ∀ n explicit descent
step624_COMPLETE.lean48Cases 5-8 sub-classes + batch_10000 + gk1-10 + strong_ind

Case 1 (t₁=1、 下降エンジン核) の Lean 4 skeleton

-- STEP 623 v3: Case 1 = trailing 1-bit が 1 個 の 奇数
-- 3n+1 → /2 → /2 で 元より 小さくなる (2 step で 3/4 倍)
theorem case1_descent (n : ℕ) (hn : n ≥ 3) (h_odd : Odd n)
    (h_t1 : trailingOnes n = 1) :
    collatz_iter 3 n < n := by
  -- Case 1 の 2 進数構造: n = ...01 の形
  -- 3n+1 = ...100、 これを 2 で 2 回 割る と ...1 で 元の n より 小
  omega_or_native_decide_finalizer

Case 5-8 (t₁ ≥ 4) の 難しさ

trailing 1-bits が j 個 の 奇数は、 3n+1 → (3/2)^j 倍 に 一気に 増加する (empirical、 j≥4 で 有限 mod 分析 不能)。 これが Collatz の 本質的困難。 Rei stack は Cases 5-8 について:

  • batch_10000: n = 12 から 10000 まで 全 orbit を Lean 4 native_decide で 機械検証済
  • strong_ind: n ≥ 10001 について 強帰納法 の skeleton を 構築、 但し induction step の sorry は 残置
  • gk1-10: mod-2^k 分析の 10 段 (k=1 から 10) だが、 k=4 以降 mod の 数が 爆発

Trailing ones 79% 壁 (STEP 690-696 empirical、 Cases 5-8 の 数値観察)

STEP 690-696 (Quadratic-log + Two-Tier + Mod-6 Dynamics + Orbit DAG + n=91 hub + Atomic Cores) で、 t₁ ≥ 4 の 領域について:

  • tier2 (t₁ ∈ {4, 5}) は empirical で 95% の n について descent (但し formal proof なし)
  • t₁ ≥ 6 の 「深い壁」 は 数値観察 のみ、 mod 分析が 有限に 収束する 保証なし
  • n=703 (t₁ が 特殊 pattern) など 個別 case を STEP 685 (Riemann 三者分類) + STEP 693 (n=91 hub) で 個別 handle

Rei stack meta index (Collatz 周辺の 関連資産)

資産関連 STEP / DOICollatz との 接続
Chang v6 29-paradigm exhaustion (20/29 axiom-free retrofit)STEP 1269 / 1293 site pageCollatz は Chang paradigm P24 (obstruction) に mapped、 T1Obstruction quadruple の 一角
Constructor Theory 5/5 axiom-free (層 4 完成)STEP 1298 site page + Deutsch-Marletto 2013-2025Collatz の 「可能性/不可能性」 を Constructor Theory 語彙で 記述 candidate
Paper 145 v0.9-c 4-substrate cross-verificationSTEP 1264 / 1292 site page + DOI 10.5281/zenodo.20091185D-FUMT₈ 8 値表現 の 物理 silicon 実装 (Tang FPGA + Aer + IBM Heron r2)、 verdict semantics の hardware 基盤
Rei-Solver v0.4 (6 engine、 万能 TM 外 3/3)STEP 1297 site pageCases 5-8 open 部分の 別経路 verification candidate
Paper 55 (Collatz 構造的証明)GitHub Release collatz-proof-v1STEP 614-624 48 定理 の 論文化 (2026-05)
Paper 57 (Collatz 8-state DFA Firewall)Rei stack Papers 索引t₁ 分類の DFA 表現
Paper 58 (Alphabet Reduction + F-Entropy)DOI 10.5281/zenodo.19504642 (Lean 4 1562 定理)Collatz + F-Entropy を 統合形式化

関連 DOI + ソースコード

researcher6. D-FUMT₈ 8 値 semantic mapping (Collatz domain)

TRUE = 1.0 (⊤) — descent 完全証明 FALSE = 0.0 (⊥) — 反例 (Collatz では未発見) BOTH = 2.0 (⊤⊥) — 複数 path 矛盾 NEITHER = -1.0 (～) — わからない / t₁ wall INFINITY = 3.0 (∞) — 無限 orbit (未発見) ZERO = 4.0 (〇) — vacuous / n=1 FLOWING = 5.0 (～→) — 進行中 SELF = 6.0 (⟲) — cycle (4→2→1→4)
D-FUMT₈ value意味Collatz condition
TRUE (⊤)descent 完全証明全 orbit step で t₁ < 4、 STEP 622-624 Lean 4 で proven
ZERO (〇)vacuous / base casen = 1 (自明)
SELF (⟲)cycle detected4 → 2 → 1 → 4 → ... の 唯一既知 cycle
FLOWING (～→)orbit 進行中実行中の中間 step (計算未完)
NEITHER (～)proof 外 (「わからない」)t₁ ≥ 4 step 出現 = Rei axiom-free scope 外、 empirical は descend
INFINITY (∞)無限 orbit未発見 (Collatz 予想 反例候補)
BOTH (⊤⊥)矛盾 pathCollatz 単独では 発生せず、 multi-verifier 併用時 marker
FALSE (⊥)反例Collatz では 未発見、 発見されれば 数学的大事件

7. Honest scope

  1. 本 v0.2 は 教材 であって Collatz 予想 の 証明 ではない。 STEP 622-624 は t₁ < 4 に限定した partial proof、 t₁ ≥ 4 の empirical descent は Lean 4 axiom-free で 未 close (「有限 mod 分析不能」)。
  2. NEITHER 判定 = 「Rei stack の 現 formal scope 外」 の marker であって、 「Collatz 予想 は 偽」 でない。 empirical は 2⁶⁸ まで 全 n descend confirmed (外部研究 by Barina 2020)。
  3. 「小学生でも 分かる」 は 予想の 説明可能性のみ、 証明の 難しさは 現代数学の 最深部 に 属する (Erdős 「数学は まだ 準備が できていない」)。 教材は 「触って驚く」 目的で、 「解けそう」 の 錯覚を 与えない。
  4. 「t₁=1 が 下降エンジン」 は STEP 623 v3 Case 1 の 直接的な言い換え、 Rei 独自 novelty 主張ではない (Terras 1976 stopping time density 系統の 既知 observation を Lean 4 axiom-free で 再形式化した 位置)。
  5. 教員向け drop-in の 「5 分で 組み込める」 は 準備時間の 目安であって、 授業効果の 保証ではない。 学年・単元・教員判断 で 適切な範囲を 選ぶ。
  6. Chang paradigm coverage 20/29 + Constructor Theory 5/5 + Paper 145 v0.9-c 4-substrate は Rei stack meta index として 提示、 Collatz と 直接接続する formal proof ではない (認識学的 mapping candidate)。
  7. ソースコード + Lean 4 file + Zenodo DOI + GitHub link は 全て 公開、 教員は 準備なしで 開ける、 研究者は 深層に 降りて 論文引用まで 到達できる。 login 不要 install 不要 の principle は 意図的 (教育到達性の 前提)。
  8. v0.3 予測記入 zone の scope 限界: 予測は optional (空欄でも verify 可)、 記入時のみ 比較 pane 表示。 予測 vs 実測 の 「学びに 変わった」 evidence は 教員 pilot 未実施のため 未計測 (v0.4 で 予測記入率 + 予測外れ 時の 継続 engagement 実測 candidate)。 POE (White & Gunstone 1992) + Mazur 1997 peer instruction pedagogy は 数学教育 general で、 「Rei stack Collatz 教材 適用で 同 効果」 は 統計理論上の 断定ではなく 合理的仮定。 STEP 1358 Statistics 教材 v0.2 で 確立した POE template を Collatz domain に 移植した 位置 = novelty は Rei stack 内 template 展開のみ、 教育学 domain の 独立発見主張なし。 hit 判定閾値 (steps 20% / maxVal 30% / t₁ ±1 / verdict exact) は Collatz orbit の カオス的性質を 考慮した 保守的 line、 domain-specific tolerance。

8. 関連 file + 履歴