find_gaps — curated Mathlib gap registry 検索

MCP tool v0.1 段 3 完成 (2026-08-20) · curated 31 entries × 3 tiers

役割: 「Mathlib に まだ無い 定理」を探すための tool。 search_verified が「あるもの」を index から substring で引くのと対称の逆向き検索。 v0.1 は Mathlib 依存グラフの自動解析は 行わない — 現状は手動 curated JSON (3 tier, 31 entry) の filter 検索のみ。依存グラフ / semantic matching は v0.2+ 側 (audit_gaps が段 4 で部分 cover)。

3 tier 構造

tier	source	count	内容
sorry-residual	`data/lean4-curated/mathlib-sorry-residual.json`	8	Mathlib4 内 sorry 残留 (PR 追跡)
unformalized	`data/lean4-curated/mathlib-unformalized.json`	15	Mathlib4 未形式化既知定理 (Wiedijk Top 100 crosscheck)
mml-missing	`data/lean4-curated/mml-missing.json`	8	MML (Mizar) 済 × Mathlib4 未移植

使い方

CLI

npm run find:gaps                                     # list all (default limit 50)
npm run find:gaps -- "fermat"                         # substring
npm run find:gaps -- --tier unformalized              # tier filter
npm run find:gaps -- --area topology --difficulty medium,low
npm run find:gaps -- --dfumt8 FLOWING,BOTH
npm run find:gaps -- "" --json                        # machine-readable

MCP

rei-aios MCP server の tool として呼び出せる (v2.7.0 の 36 tool の 1 つ)。

返却 payload の field (drift audit 済)

field	意味
`hits[]`	ヒット配列
`hits[].entry.id`, `tier`, `name`, `area`, `description`	curated entry 本体
`hits[].entry.difficulty`, `dfumt8`, `references[]`	metadata
`hits[].entry.mathlibPath?`	sorry-residual tier のみ (該当 file path)
`hits[].entry.mmlArticle?`, `mmlAuthor?`	mml-missing tier のみ
`hits[].entry.wiedijkRank?`, `knownPRs?`, `estimatedYears?`	tier-specific
`hits[].matchedIn`, `score`	一致箇所 + ranking
`totalMatches`	filter 後の全 match 数 (limit 前)
`totalReturned`, `tierCounts`	返却件数 + tier 別集計
`registryLastUpdate`, `registryVersion`	curated registry snapshot 日時 + version
`loadedFiles`, `missingFiles`	読み込めた/欠落 JSON
`honestScope`	制約明示

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

手動 curated data のみ — Mathlib 依存グラフの自動解析は含まない (v0.2+ scope、 audit_gaps が部分 cover)。
Registry lastUpdate = 2026-04-27 (~4 か月前)。それ以降に埋まった gap は反映されない。 audit_gaps を回すことで検出可能 (それが段 4 の存在理由)。
「無い」の判定は curator が Mathlib 4 main branch snapshot 比較した時点のもの。
Substring 検索のみ — 数式・同値な言い換えの探索は未対応 (false negative あり得る)。
find_gaps を Mathlib PR / 論文の「これが未形式化」主張の 唯一 evidence にしてはいけない。主張前の手動 grep audit (feedback_mathlib_grep_before_novel_gap_claim.md) が依然 primary。

Rei stack 位置付け

2026-08-19 合意 Order 原則の段 3。 search_verified の逆向き / audit_gaps の入力。詳細は三段 arc research-log。