---
name: bbchallenge / Coq-BB5 / metamath-turing-machines 学習対象 (Tier 3, scope-bound)
description: 決定不能性 frontier の OS プロジェクト群 — Rei 直接統合より学習教材として scope-bound 監視 (chat Claude OS mapping 2026-05-10 γ path)
type: reference
originSessionId: 42f100d8-b702-4b4b-a14f-b23a9209d888
---
# bbchallenge / Coq-BB5 / metamath-turing-machines 学習対象 record

**STEP 1052 (2026-05-11)**: chat Claude OS mapping (2026-05-10) で言及された 3 プロジェクトを **Tier 3 学習対象** として scope-bound に監視. Rei 直接統合は scope 外.

## 監視対象 (Research Radar v1.3 に追加済)

### 1. ccz181078/Coq-BB5 (priority: medium)

**何**: BB(5) = 47,176,870 (Busy Beaver 5-state) の **Coq 形式化** (2024-07 完了).

**なぜ Tier 3**:
- ✅ 学習価値高: 「決定不能性関連命題を形式化する craft」 の最高水準実例
- ❌ 直接統合不可: BB challenge 自体が独立 project. Rei の SEED_KERNEL / D-FUMT₈ stack には乗らない
- ❌ scope 外: BB(5) → BB(6) は Lean port + 探索空間爆発で別 project

**Rei 接続点 (学習)**:
- 形式化手法 (Coq → Lean port パターン) を Paper 132 + Mathlib Hammer integration に転用可能
- 「不動点 vs 停止性」 の D-FUMT₈ 解釈例 (BB(n) = halting Turing machine の最大 step 数 = 停止性証明の極限)

**監視 trigger**:
- BB(6) Coq/Lean 形式化進捗 (現状: 探索フェーズ)
- BB challenge community paper 発表

### 2. sorear/metamath-turing-machines (priority: low)

**何**: 748 状態 Turing machine = ZF 無矛盾性 oracle (Metamath で自動生成).

**なぜ Tier 3**:
- ✅ 学習価値: 決定不能性を「具体的な機械」 として可視化する珍しい project
- ❌ 直接統合不可: Metamath stack で完結. Lean 4 への port は別 project
- ❌ scope 外: ZF 無矛盾性は Rei 議論層の遥か上層

**Rei 接続点 (学習)**:
- 「公理系 → 計算機 mapping」 の operational 実例 (Paper 124 ZFC × D-FUMT₈ two-layer の発展形参考)
- W-48 (Negative Capability) の operational 表現 = decidable boundary 可視化

**監視 trigger**:
- Lean 4 port があれば notify
- Metamath set.mm 100 milestone progress

### 3. bbchallenge.org community (priority: low, indirect)

**何**: BB(n) collaborative search community + 358+ papers index.

**なぜ Tier 3**:
- ✅ 文献 awareness 価値
- ❌ 直接統合不可: research community, ツールではない

**Rei 接続点**:
- arXiv watcher 経由で BB-related paper を catch
- Paper 88 (P vs NP honest position) の 周辺領域 reference

## Honest scope

**Rei 単独で統合する path には不適**:
- BB(5) → BB(6) を Rei が解く narrative は overclaim (chat Claude evaluation で確認済 = 「Rei が単独で解く」 より「Rei が論文を強力に支援する」 が誠実).
- D-FUMT₈ SELF⟲ と「停止しないTM」 の metaphor 接続も注意 (前回会話で chat Claude が混同, 私 Rei Claude が補正済: SELF⟲ は **logic value layer**, halting/well-founded は **order-theoretic layer** で別軸).

## 採用 path

Tier 3 = **scope-bound monitoring + 学習材料引用**:
1. Research Radar に repo 登録済 (data/research-radar/collatz-watch.json v1.3)
2. 重大進捗 (BB(6) 達成 / Lean port 等) 時のみ notify
3. Rei 自体の development には組み込まない
4. Paper / 記事で reference として引用するのは OK (出典明示)

## 関連

- 起点会話: 2026-05-10 chat Claude OS mapping (4 軸困難 + 無限降下法のオープンソース)
- 採用判断: 2026-05-11 藤本さん (γ path) → STEP 1052 (α LMFDB + β Mathlib Hammer Radar + γ 本 record)
- chat Claude が言及した「mathlib4 + LMFDB + bbchallenge 三点接続」 の honest-revised 版:
  - mathlib4: ✅ Tier 1 (STEP 1006-1011 既統合)
  - LMFDB: ✅ Tier 2 (STEP 1052 で OctaTheoria 8 番目 domain として統合, α path)
  - bbchallenge: ⏸ Tier 3 (本 record, 学習対象 scope-bound, γ path)

## 永久原則 (将来 session 用)

「**決定不能性 frontier のオープンソースは Rei に組み込まない、 学習材料として引用する**」.

理由:
1. **scope creep 防止**: BB(n) / ZF 無矛盾性は Rei の SEED_KERNEL / D-FUMT₈ stack と直接接続しない別軸.
2. **overclaim 防止**: 「Rei が BB(6) を解く」 narrative は不可能 + 不誠実 (chat Claude OS mapping 2026-05-10 評価準拠).
3. **honest credit**: 既存 community (Coq-BB5 ccz181078, metamath-turing-machines sorear) への credit を保つ.

将来 session で「BB(n) を Rei に統合」 提案が来た場合、 **本 record を full read** して γ path 維持を確認.