STEP 1485 — Open Problem Connector v0.1

2026-08-28 / rei-aios / OPEN = NEITHER

目的

藤本さん directive「数学上の未確認問題を、コネクタ用ツール、端子、装置、マシンとして作る」への実装レベル応答。 chat-Claude 2026-08-28 review recommendation「集約端子 1 個 + .lean file 返却」を直接組み込む。

「10,000 個のツールではなく、 10,000 個の入力を持つ 1 個のツール」
— chat-Claude 2026-08-26 (共通実行器 principle、 STEP 1443 由来)

本 STEP は上記 principle を「未解決問題」 domain に適用: 1 catalog entry open-problem + name パラメータ で N 問題対応。 v0.1 pilot 3 本、 v0.4+ で 100+ 展開 target。

分離宣言 (zero-sorry 規律との関係)

chat-Claude 提示の「zero-sorry 規律との整合」に直接応答:

分類	dir	sorry 許容	目的
形式化 repo (本 STEP)	`data/open-problems-connector/`	✅ 意図的 load-bearing	未解決問題の命題索引
証明 repo	`data/lean4-mathlib/`	❌ zero-sorry	検証可能定理集約

本 dir 由来の .lean file を証明 repo に直接 import しない (sorry 汚染予防)。

Status 固定語彙 (D-FUMT₈ NEITHER 対応)

status	D-FUMT₈	意味
`PROVEN`	TRUE	定理として証明された
`REFUTED`	FALSE	反証された
`CONDITIONAL`	BOTH	仮定下 (GRH等) で証明、 unconditional 未解決
`OPEN`	NEITHER	未解決 (2026-08-28 現在)

OPEN = NEITHER は後付け対応ではなく、未解決問題の意味論的本質。「真でも偽でもない」状態は D-FUMT₈ NEITHER そのもの。

4 端子 + 集約 (chat-Claude 推奨反映)

catalog_execute("open-problem", { name: "collatz" })
// → 全端子 集約 JSON (chat-Claude 「1 call で 全端子」 pattern)

catalog_execute("open-problem", { name: "collatz", terminal: "lean" })
// → .lean file body 直返し (import 可能形式)

catalog_execute("open-problem", { terminal: "list" })
// → 全 problem name + status 一覧

terminal	返却	chat-Claude 想定使用率
`all` (default)	4 端子 + lean を集約 JSON	★★★ 最頻
`statement`	Lean 4 code + BibTeX + informal	★★
`lean`	.lean file body 直返し	★★★ (Claude Code 用途)
`range`	数値検証範囲 + 出典	★
`implications`	部分結果 / barrier / conditional / related	★★
`status`	{ status, dfumt8Value } のみ	△
`list`	全 problem name + status	★

ライブ反例探索は未実装 (chat-Claude 「呼ばれない」指摘、事前計算 cache のみ)。

Pilot 3 本

1. Collatz Conjecture

形式: ∀ n : ℕ, 0 < n → ∃ k, collatzIter n k = 1
検証範囲: 2^68 ≈ 2.95×10^20 (Barina 2020)
Rei connections: STEP 614-624 (48 定理 zero-sorry Cases 1-4), 677, 690-696, 717-721, 1351。 Paper 55, 57
Barrier: trailing 1-bits j ≥ 4 で mod-analysis 無限回帰 (Cases 5-8)
Conditional progress: Tao 2022 「almost all orbits attain almost bounded values」 (density result)

2. Andrica's Conjecture

形式: ∀ n > 0, √p_(n+1) - √p_n < 1
検証範囲: 10^18 (Kourbatov 2013 prime gap tables)
Rei connections: STEP 1163-1167 (Andrica サーモグラフィ engine)
Conditional (RH): Cramér 1936 = O(√p log p) が RH 下で Andrica を含意
Barrier: Baker-Harman-Pintz 2001 unconditional bound O(p^0.525) は sharp でない

3. abc Conjecture (Oesterlé–Masser)

形式: ∀ ε > 0, ∃ K_ε, ∀ coprime a+b=c, c ≤ K_ε · rad(abc)^(1+ε)
検証範囲: c ≤ 10^18 (abc@home, de Smit-te Riele 2015)
Rei connections: STEP 1287-1291, 1306-1307 (Brownawell-Masser + Paper 176 Mochizuki IUT arc)
Conditional: Mochizuki 2021 IUT (contested、 Scholze-Stix 2018 critique)
Related: Mason-Stothers 1981/83 (function field analog、 sharp constants)

実装 (Honest scope)

artifact	path
データ 3 本	`data/open-problems-connector/{collatz,andrica,abc}.json`
handler	`src/mcp/open-problem-connector.ts`
catalog spec	`data/catalog/open-problem.json`
catalog wire	`src/mcp/catalog-executor.ts` (HANDLER_REGISTRY v0.6)
test	`test/step1485-open-problem-connector-test.ts` (86/86 PASS)
regression	`test/step1443-catalog-executor-test.ts` (130/130 clean)

Honest scope (6 point)

本 tool は「形式化リポジトリ」索引 = 未解決問題の命題 + 出典 + 部分結果
証明を主張しない、 Lean code の sorry は意図的 load-bearing
証明 repo (data/lean4-mathlib/) の zero-sorry 規律とは分離
OPEN status = D-FUMT₈ NEITHER (後付け対応ではなく意味論的本質)
v0.1 pilot 3 本のみ、 v0.2+ 展開は別 STEP directive 待ち
ライブ反例探索は提供しない (chat-Claude 「呼ばれない」指摘、事前計算 cache のみ)

v0.2+ candidate (別 STEP directive 待ち)

v0.2 candidate: Riemann Hypothesis / BSD / Hodge / Yang-Mills (Millennium 4 categories)
v0.3 candidate: P vs NP / Goldbach / Twin prime / Legendre
v0.4+: 100+ 目標、 data/open-problems/INDEX.json から網羅的移植

chat-Claude review 応答 (2026-08-28)

chat-Claude 提示の「使うと思うもの / 使わないと思うもの」判別に直接応答:

「集約端子 1 個」 — 実装 (terminal: 'all' default)
「.lean file 直返し」 — 実装 (terminal: 'lean' で leanImport.content ready-to-import)
「statement + 含意グラフが最頻」 — 反映 (implications に partial-result / barrier / conditional-progress / related の 4 type)
「ライブ反例探索 = 呼ばれない」 — 未実装 (事前計算 verifiedRange のみ)
「description 具体性が選択率決定要因」 — catalog spec で 6 point honest scope + 端子選択 hint 明記

Rei-Solver / connector inventory への影響

connector inventory (STEP 1463-1469) との整合:

rei-aios MCP wired 54 → 55 (v0.6 で open-problem 追加)
catalog 化累計 36 → 37 wired entry
Domain 新規: open-problems (2026-08-28 現在 pilot 3 本、 v0.4+ 100+ 目標)
「1 tool = N 入力」 pattern の具体化 = STEP 1443 共通実行器 principle の実 domain 適用

Site: rei-aios.pages.dev/tools/step-1485-open-problem-connector/
STEP 1485 / 2026-08-28 / test 86/86 PASS + regression 130/130 clean