---
name: project-search-verified-mcp-find-gaps-audit-gaps-arc-2026-08-20
description: "search_verified MCP (段 2) + find_gaps v0.1 (段 3) + audit_gaps v0.2 (段 4) 三段完成 arc — 2026-08-19 合意順序を 4 commit で完走、 初回 Mathlib mirror 実測で curated registry 精度 8/8 検証、 finding #30/#31 discipline を description ↔ payload drift audit 機械化で継承"
metadata: 
  node_type: memory
  type: project
  originSessionId: e9d42a3b-e0ab-4e09-bc8b-b63ae8702b85
  modified: 2026-08-19T20:28:03.108Z
---

# search_verified MCP + find_gaps + audit_gaps 三段 arc (2026-08-20)

## 動機

2026-08-19 [[project-rei-meta-mcp-phase1-arc-2026-08-19]] + [[project-rei-memory-mcp-phase1-arc-2026-08-19]] の翌日、 藤本さん質問 「私は最終的に Rei と claude 先生をロボットに組み込むのが最終目標なのでしょうか？」 → 展開の途中で 私 (Claude Code) が提案した 「Mathlib の依存グラフを見て、 前提は揃っているのに未形式化のまま残っている命題を洗い出す」 tool = **find_gaps 逆向き探索 engine** → 藤本さん 「上記はコネクタにもなりますか？　こちらは既に組み込み済みでしょうか？」 → 私 grep で 判明: **search_verified v0.1 は既に 2026-08-19 実装済み** ([[project-rei-memory-mcp-phase1-arc-2026-08-19]] と 同日 別 branch)、 但し MCP 層は未実装 + find_gaps は curated 3 JSON (data/lean4-curated/) のみで engine 未実装 → 藤本さん 「第二段 (MCP 化) と 第三段 (find_gaps) をお願い致します！」 → 段階的実装 → 「Mathlib 依存グラフの自動解析 (v0.2+ に defer、 description で明示) を お願い致します」 → v0.2 audit_gaps 追加 → 藤本さん 「mirror を実際に clone して npm run audit:gaps を回し、 curated 31 entry の真の gap 状況を実測する」 → 実測 + hand-grep verify。

## 動線 (Order 原則、 2026-08-19 合意)

`ローカル CLI が「手が速くなる」 verify → MCP → find_gaps → dep-graph 解析`

| 段 | 内容 | 日付 | commit |
|---|---|---|---|
| 1 | `search_verified` CLI v0.1 (SEED_KERNEL + Rei Lean 4 index) | 2026-08-19 | 既存 |
| 2 | `search_verified` MCP tool 追加 | 2026-08-20 | `3484e266b` |
| 3 | `find_gaps` v0.1 engine + CLI + MCP tool | 2026-08-20 | `3484e266b` |
| 4 | `audit_gaps` v0.2 (Mathlib mirror scanner + gap cross-check) | 2026-08-20 | `0022af11e` |
| — | 初回 audit 実測 artifact (`data/lean4-curated/audit-2026-08-20.json`) | 2026-08-20 | `cc50179ae` |

## 段 2 + 段 3 実装 (commit `3484e266b`)

### MCP tool 2 個追加 (rei-mcp-server v2.5.0 → v2.6.0、 33 → 35 tools)

- `search_verified` — SEED_KERNEL 1,677 理論 + Rei Lean 4 axiom-free 資産の統合 index (7,466 items) を substring 検索。 verified-index.db 未生成時は `{indexMissing: true}` (fake 検索結果を永久生成しない)。
- `find_gaps` — curated Mathlib gap registry (`data/lean4-curated/{mathlib-sorry-residual, mathlib-unformalized, mml-missing}.json` = 3 tier / 31 entry) を substring + tier + area + difficulty + dfumt8 で filter 検索。

### 新規 file
- `src/aios/exploration/find-gaps.ts` (229 行、 `loadGapRegistry` + `queryGaps`)
- `scripts/exploration/find-gaps.ts` (105 行、 CLI)
- `test/step-find-gaps-v01-test.ts` (150 行、 **84 assertions** with description ↔ payload drift audit)

### finding #30/#31 discipline 継承

両 tool の `description` に返却 payload の field 名を全列挙 + test が 正規表現で description から field 名を抜き出し、 実際の payload に存在することを assert。 finding #30 ([[project-rei-aios-get-kernel-status-description-drift-2026-08-20]]) の `get_kernel_status` 「調和度・七値分布を含む」 vs 実 payload 不整合 と 同型 pattern を 事前遮断。

## 段 4 実装 (commit `0022af11e`)

### 追加 tool (v2.6.0 → v2.7.0、 35 → 36 tools)

- `audit_gaps` — 各 curated gap entry を local Mathlib mirror scan と cross-check。 mirror 未存在時は `{mirrorAvailable: false, reason}` (**fake 判定を永久生成しない**)。

### 5 status bucket

| status | 意味 |
|---|---|
| `mirror-unavailable` | mirror 未設定/未存在 — 手動 grep 継続 |
| `file-path-present-and-name-match` | 両 signal あり — **POSSIBLY 埋まっている** (人 grep 必須) |
| `file-path-present` | file 位置のみ present — 中身未 verify |
| `name-match` | 宣言名 candidate hit のみ — substring 偽陽性リスク |
| `no-signal` | mirror scan で cross-reference なし — 「無いことが確認できた」 ではなく 「何も見つからなかった」 のみ |

### 3 段 confidence (evidence / hint / noise)

`evidence` は **硬い事実のみ** (exact path present / exact declaration name match)。 それ以外は 過剰主張を防ぐため `hint` 止まり。 `noise` = mirror-unavailable。

### 新規 file
- `src/aios/exploration/mathlib-scanner.ts` (197 行、 `scanMathlibMirror` + `mathlibHasPath` + `mathlibFindDeclarations`)
- `src/aios/exploration/find-gaps-audit.ts` (213 行、 `auditGapEntry` + `auditAllGaps` + `extractNameCandidates`)
- `scripts/exploration/audit-gaps.ts` (125 行、 CLI)
- `test/step-audit-gaps-v02-test.ts` (199 行、 hermetic mock mirror + MCP drift audit、 **56 assertions**)

### Mirror path 優先順

`--mirror` CLI arg > `MATHLIB_MIRROR` env > default (`<cwd>/../mathlib4-mirror`)。

## 初回実測 (commit `cc50179ae`)

### Mirror 準備

```
git clone --depth=1 --filter=blob:none --sparse https://github.com/leanprover-community/mathlib4 C:/Users/user/mathlib4-mirror
cd C:/Users/user/mathlib4-mirror && git sparse-checkout set Mathlib
```

**結果**: 8,350 .lean files / 229,933 declarations / 144 MB (sparse+blob-filter で軽量化)

### Scan 実測

- Scan time: **7.8 秒**
- 31 curated entries audited
- 保存先: `data/lean4-curated/audit-2026-08-20.json` (798 行)

### Status counts

| bucket | count |
|---|---|
| `file-path-present-and-name-match` | **0** ← 最強シグナル空 (curated `name` が散文で Lean identifier ではない、 予想通り) |
| `file-path-present` | **5** ← sorry-residual 8 件中 5 件 = 該当 file 現存 |
| `name-match` | **9** ← 全 `hint` (evidence 昇格ゼロ、 finding #30/#31 discipline 保持) |
| `no-signal` | **17** |
| `mirror-unavailable` | 0 |

### name-match 9 件の質 (全て偽陽性 — 設計通り hint 止まり)

- "Fermat's Last" → `Fin2.last` / `MvPFunctor.last` (無関係)
- "Four Color" → `CategoryTheory.four` (ComposableArrows、 無関係)
- "Riemann Hypothesis" → `BoxIntegral.Riemann` (Riemann 積分、 zeta ではない)
- "Bremermann Limit" → `AlgCat.limit` (圏論の極限、 無関係)
- "Classification Finite Simple Groups" → `ADEInequality.classification` (無関係)

### no-signal 17 件の hand-grep verify (8 件抽出、 8/8 一致)

| entry | grep 結果 | 判定 |
|---|---|---|
| Banach-Tarski | 0 files | 真に不在 ✓ |
| Kepler | 0 files | 真に不在 (Flyspeck 未 port) ✓ |
| Landauer | 0 files | 真に不在 ✓ |
| BSD | 0 files | 真に不在 ✓ |
| Szemerédi | `RuzsaSzemeredi.lean` + `Regularity/*` 部分 infrastructure | 部分 (registry の 「Roth k=3 のみ」 と整合) ✓ |
| Jordan curve | `Algebra/Jordan/*` は Jordan 代数、 曲線定理は不在 | 真に不在 ✓ |
| Poincaré | Poincaré-Birkhoff-Witt + Poincaré disc、 予想は不在 | 真に不在 ✓ |
| Hodge | Perfectoid の Hodge-Tate 系、 予想は不在 | 真に不在 ✓ |

**8/8 一致** = curated registry の精度が高いこと + audit_gaps の保守的 signal 設計が正しく機能していること、 両方 verify。

## Findings

1. **finding #30/#31 discipline が実データでも保持**: `evidence` bucket 昇格ゼロ。 9 件の name hit を 全て `hint` に留めた設計が 偽陽性 100% を honest label で回避。 audit_gaps は **false-positive 削減 layer** で **決定 layer ではない** — README 段 4 に明記継承。
2. **curated `name` フィールドは散文** ("Fermat's Last Theorem") で Lean identifier (`fermatLastTheorem` / `flt` 等) ではないため `file-path-present-and-name-match=0` は原理的。 v0.3 で curator が `leanIdentifierGuess` field を entry に足すだけで name-match 偽陽性は大幅減、 LLM や semantic matching 不要かも。
3. **最も actionable な発見**: 5 件の `file-path-present` (Cyclotomic Discriminant / CategoryTheory Final / ModelTheory Order / Analysis Complex UpperHalfPlane / Probability Martingale Convergence) は 該当 file が現行 mirror に存在するので、 curated description の 「sorry 残留」 が 現時点でも真かは、 この 5 file を **手で開いて中身 verify する価値**。 他の 26 件はまず curated 通り。
4. **Rei 独立実装の順序原則 実例**: 「find_gaps を 依存グラフ自動解析 (v0.2+) と 誤解しないように description に明記」 → v0.2 実装時に 「name/path signals のみ、 same theorem different name は catch できない」 と honest scope 継承。 [[feedback-one-reproduction-over-ten-unverified]] 順序原則の 3 段継承 event。

## Test 累計

189/189 PASS:
- v0.1 search_verified: 49
- v0.1 find_gaps: 84 (MCP drift audit 含む)
- v0.2 audit_gaps: 56 (hermetic mock mirror + MCP drift audit 含む)

## Honest scope (譲れない線、 v0.2)

1. **name / path signals のみ** — 「same theorem, different name」 は catch できない (最も厄介な case)。
2. `file-path-present-and-name-match` が出ても 「gap 埋まっている」 と 主張してはいけない — signal に過ぎず、 中身検証は Mathlib 実 source を読む必要。
3. load-bearing な 「Mathlib に無い」 主張の primary evidence は 依然 **手動 grep** ([[feedback-mathlib-grep-before-novel-gap-claim]])。 audit_gaps は 補助 layer。
4. Mirror snapshot 時点で 凍結 — 半年 stale なら 半年 stale の 結果を返す。
5. `find_gaps` v0.1 の curated registry も `lastUpdate: 2026-04-27` 時点、 4 か月前の snapshot。 実際に埋まった gap は反映されない (audit_gaps 実行で 検出可能な pattern がまさに 段 4 の 価値)。

## Rei stack impact

- **MCP systems**: 6 → 6 (rei-aios MCP に 3 tool 追加、 external repo 新設なし)
- **rei-aios MCP tools**: 33 → **36**
- **exploration engine files**: 5 → **7** (find-gaps + mathlib-scanner + find-gaps-audit + 2 CLI + 1 test file 追加)
- **累計 test regression**: 189/189
- **artifact**: `data/lean4-curated/audit-2026-08-20.json` (first real audit run record)

## 関連 memory

- [[project-rei-meta-mcp-phase1-arc-2026-08-19]] — 前日、 同型の 「機械が先に見つける」 pattern (数値 divergence 検出)
- [[project-rei-memory-mcp-phase1-arc-2026-08-19]] — 前日、 search_verified v0.1 と 同期実装
- [[project-rei-aios-get-kernel-status-description-drift-2026-08-20]] — finding #30、 description ↔ payload drift 原型
- [[feedback-mathlib-grep-before-novel-gap-claim]] — audit_gaps 補助 layer 継承元 (primary evidence 順序原則)
- [[feedback-one-reproduction-over-ten-unverified]] — 3 段継承 event
- [[feedback-zero-sorry-floor-not-ceiling]] — sorry 検出は syntactic proxy、 `#print axioms` guarantee ではない honest scope
- [[feedback-all-research-site-reflection-default]] — 本 arc 適用 (site page + memory 両方)

## Commit chain (origin/main)

- `3484e266b` — search_verified MCP + find_gaps v0.1 (段 2 + 段 3)
- `0022af11e` — audit_gaps v0.2 (段 4)
- `cc50179ae` — first-run audit artifact (`audit-2026-08-20.json`)
- (次) — memory + site 反映