find_gaps」 を grep で 既に 段 1 (search_verified CLI) が 実装済み と発見 (前日 2026-08-19、 [[project-rei-memory-mcp-phase1-arc-2026-08-19]] と同期)。 藤本さん 「第二段 (MCP 化) と 第三段 (find_gaps) を お願い致します」 → 段階的実装 → v0.2 dep-graph 解析 の defer + name/path signals 実装 → 実 Mathlib mirror clone + 31 entry 実測。
| 段 | 内容 | 日付 | 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 | ✓ |
SEED_KERNEL 1,677 理論 + Rei Lean 4 axiom-free 資産 (合計 7,466 items) を substring 検索。 verified-index.db 未生成時は {indexMissing: true} を返し、 fake 検索結果を永久に生成しない。 v0.1 の Lean parser は regex-based、 lean4Verified は syntactic proxy (#print axioms guarantee ではない、 honest scope 継承)。
curated Mathlib gap registry (data/lean4-curated/ 3 tier / 31 entry) を substring + tier + area + difficulty + dfumt8 で filter 検索。 v0.1 は 手動 curated data のみ で Mathlib 依存グラフの自動解析は含まない (v0.2+ scope、 description で明示継承)。
各 curated gap entry を local Mathlib mirror scan と cross-check、 5 status bucket で per-entry 結果を返す。 Mirror path 優先順: --mirror > MATHLIB_MIRROR env > default (<cwd>/../mathlib4-mirror)。 未存在時は {mirrorAvailable: false, reason} + reproduce 用 shallow-clone command を返し、 fake 判定を永久に生成しない。
| status | 意味 |
|---|---|
file-path-present-and-name-match | 両 signal あり — POSSIBLY 埋まっている (人 grep 必須) |
file-path-present | file 位置のみ present — 中身未 verify |
name-match | 宣言名 candidate hit のみ — substring 偽陽性リスク |
no-signal | cross-reference なし — 「無いことが確認できた」 ではなく 「何も見つからなかった」 のみ |
mirror-unavailable | mirror 未設定/未存在 — 手動 grep 継続 |
各 signal の confidence は 3 段:
get_kernel_status description 「調和度・七値分布を含む」 vs 実 payload 5 field で 「調和度」 「七値分布」 両方不在) + finding #31 (rei-meta 自身の verdict/status drift) の直後、 本 arc で新規 3 tool を追加する。 同型 drift の再発防止が必須。
description に返却 payload の field 名を 全列挙 + test が 正規表現で description から field 名を抜き出し、 実際の payload に存在することを assert (test/step-find-gaps-v01-test.ts + test/step-audit-gaps-v02-test.ts)。 drift audit の機械化。 audit_gaps の場合 15 field 全て assert 済。
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 / scan 7.8 秒
| bucket | count | 解釈 |
|---|---|---|
file-path-present-and-name-match | 0 | 最強シグナル空 — curated name が散文で Lean identifier ではないため、 原理的 |
file-path-present | 5 | sorry-residual 8 件中 5 件 = 該当 file 現存 (中身の sorry 現況は手動 open 必要) |
name-match | 9 | 全 hint (evidence 昇格ゼロ、 discipline 保持) |
no-signal | 17 | cross-reference なし |
mirror-unavailable | 0 | — |
| curated entry | matched declaration | 実質 |
|---|---|---|
| Fermat's Last Theorem | Fin2.last / MvPFunctor.last | 無関係 (last = 最後の要素) |
| Four Color Theorem | CategoryTheory.four | 無関係 (ComposableArrows) |
| Riemann Hypothesis | BoxIntegral.Riemann | Riemann 積分、 zeta ではない |
| Bremermann Limit | AlgCat.limit / ModuleCat.limit | 圏論の極限 |
| Classification Finite Simple Groups | ADEInequality.classification | 無関係 |
| Lebesgue Decomposition | CategoryTheory.decomposition | 無関係 |
| Stone-Weierstrass lattice | PeriodPair.lattice | Weierstrass 楕円関数の周期格子 |
hint に留めた = evidence bucket 昇格ゼロ。 「NOTE: token substring match — false positive likely」 が detail に自動付与。 保守的設計が 実データで 100% 偽陽性を honest label で回避した実例。
| entry | grep 結果 | 判定 |
|---|---|---|
| Banach-Tarski | 0 files | 真に不在 |
| Kepler (Flyspeck) | 0 files | 真に不在 (未 port) |
| Landauer | 0 files | 真に不在 |
| BSD 予想 | 0 files | 真に不在 |
| Szemerédi | RuzsaSzemeredi.lean + Regularity/* 部分 infrastructure | 部分 (registry 「Roth k=3 のみ」と整合) |
| Jordan curve | Algebra/Jordan/* は Jordan 代数、 曲線定理は不在 | 真に不在 |
| Poincaré 予想 | PBW + Poincaré disc、 予想は不在 | 真に不在 |
| Hodge 予想 | Perfectoid の Hodge-Tate 系、 予想は不在 | 真に不在 |
Mathlib/NumberTheory/Cyclotomic/Discriminant.leanMathlib/CategoryTheory/Limits/Final.lean (Cofinal)Mathlib/ModelTheory/Order.lean (Omega Minimal)Mathlib/Analysis/Complex/UpperHalfPlane (Analytic Continuation)Mathlib/Probability/Martingale/Convergence.lean (L^p convergence)該当 file が現行 mirror に存在する = curated description の 「sorry 残留」 が 現時点でも真かは、 この 5 file を 手で開いて中身 verify する価値。 audit_gaps 本 arc の 最も actionable な output。
search_verified: 49 (既存)find_gaps: 84 (MCP drift audit 含む)audit_gaps: 56 (hermetic mock mirror + MCP drift audit 含む)leanIdentifierGuess field を entry に足すだけで name-match 偽陽性は大幅減、 LLM や semantic matching 不要かも。file-path-present-and-name-match が出ても 「gap 埋まっている」 と 主張してはいけない — signal に過ぎず、 中身検証は Mathlib 実 source を読む必要。feedback_mathlib_grep_before_novel_gap_claim.md)。 audit_gaps は 補助 layer。find_gaps v0.1 の curated registry も lastUpdate: 2026-04-27 時点、 4 か月前の snapshot。 実際に埋まった gap は 再 curate まで反映されない。data/lean4-curated/audit-2026-08-20.json (first real audit run record)project_search_verified_mcp_find_gaps_audit_gaps_arc_2026-08-20.md3484e266b → 0022af11e → cc50179ae → (本 site + memory)project_rei_meta_mcp_phase1_arc_2026-08-19 (前日、 同型 pattern 「機械が先に見つける」) / 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 原型) / feedback_mathlib_grep_before_novel_gap_claim (primary evidence 順序原則) / feedback_one_reproduction_over_ten_unverified (順序原則 3 段継承)