audit-2026-08-20 — Mathlib mirror × curated gap cross-check

読み方: 各 entry は curated gap registry (「Mathlib に無い」 と curator が判定した定理) の 1 件。 status は audit_gaps が Mathlib mirror scan で見つけた signal の 総合。 status が file-path-present-and-name-match だからといって 「gap 埋まっている」 とは 主張しない — 中身検証は Mathlib 実 source を 手で 読む 必要。 詳細な honest scope は audit_gaps tool page。

読み込み中… (raw JSON を fetch します)