audit_gaps — gap × Mathlib mirror cross-check

MCP tool v0.2 段 4 完成 (2026-08-20) · 初回実測: 8,350 files / 229,933 declarations / scan 7.8s

役割: find_gaps の curated registry が「まだ埋まっていない」と主張する entry を、実際の Mathlib mirror scan と cross-check する。 false positive を削減する layer であり、 gap の真偽を決定する layer ではない。 Mirror 未存在時は {mirrorAvailable: false, reason} で fake 判定を永久生成しない。初回実測 report: audit-2026-08-20 viewer。

Mirror セットアップ (一度きり)

git clone --depth=1 --filter=blob:none --sparse \
  https://github.com/leanprover-community/mathlib4 \
  C:/path/to/mathlib4-mirror
cd C:/path/to/mathlib4-mirror
git sparse-checkout set Mathlib

# ~144 MB, 8,350 files, scan は 7.8 秒 (Rei repo 側で MATHLIB_MIRROR env で指定)
export MATHLIB_MIRROR=C:/path/to/mathlib4-mirror

Mirror path 優先順: --mirror CLI arg > MATHLIB_MIRROR env > default (<cwd>/../mathlib4-mirror)。

5 status bucket

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 継続

3 段 confidence

evidence 硬い事実のみ (exact path present / exact declaration name match)
hint token hit / path-missing signal
noise mirror-unavailable など

使い方

CLI

npm run audit:gaps                                     # 全 31 entry
npm run audit:gaps -- --mirror C:/path/to/mathlib4-mirror
npm run audit:gaps -- --tier unformalized --limit 5
npm run audit:gaps -- --json > audit-report.json

MCP

rei-aios MCP server の tool として呼び出せる (v2.7.0 の 36 tool の 1 つ)。引数: mirror, tier, area, limitEntries, limitVerdicts。

返却 payload の field (drift audit 済)

field	意味
`mirrorAvailable`, `mirrorPath`, `scannedAt`	mirror 状態
`totalEntries`	audit 対象 entry 数
`statusCounts`	5 bucket 集計
`verdicts[]`	per-entry 判定配列
`verdicts[].gapId`, `status`, `summary`	判定本体 (summary は over-claim 禁止文面)
`verdicts[].signals[].kind`	`file-path` or `declaration-name`
`verdicts[].signals[].confidence`	`evidence` / `hint` / `noise`
`verdicts[].signals[].detail`	signal 詳細 (偽陽性リスク明示付き)
`verdicts[].signals[].matches?[]`	Mathlib decl 位置 (name / qualifiedGuess / file / line / kind)
`honestScope`	制約明示

初回実測 (2026-08-20)

Mathlib mirror scan 済み、 curated 31 entry を audit:

file-path-present-and-name-match: 0 (最強 bucket 空、 curated name が散文で Lean identifier ではないため原理的)
file-path-present: 5 (sorry-residual 8 中 5、手で file を開いて sorry 現況を verify する価値)
name-match: 9 (全 hint、 evidence 昇格ゼロ = 全て偽陽性を honest label で回避)
no-signal: 17 (hand-grep 8/8 一致で curated 通り verify 済)

Full report: audit-2026-08-20 viewer / raw JSON: /data/lean4-curated/audit-2026-08-20.json

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

name / path signals のみ — 「same theorem, different name」は catch できない (最も厄介な case)。 v0.3 candidate: curator が leanIdentifierGuess field を entry に足すだけで name-match 偽陽性は大幅減。
file-path-present-and-name-match が出ても 「gap 埋まっている」と主張してはいけない — signal に過ぎず、中身検証は Mathlib 実 source を読む必要。
load-bearing な「Mathlib に無い」主張の primary evidence は依然 手動 grep (feedback_mathlib_grep_before_novel_gap_claim.md)。 audit_gaps は補助 layer。
Mirror snapshot 時点で凍結 — 半年 stale なら半年 stale の結果を返す。
find_gaps v0.1 の curated registry も lastUpdate: 2026-04-27 で 4 か月前 snapshot。

Rei stack 位置付け

2026-08-19 合意 Order 原則の段 4。段 3 find_gaps の false-positive 削減 layer。全体の詳細は三段 arc research-log。