From fbb6b777b0c506baf25a562cab6d0c16839a2e92 Mon Sep 17 00:00:00 2001 From: suzuki Date: Mon, 4 May 2026 11:35:47 +0000 Subject: [PATCH 1/5] docs: introduce Karpathy-style working principles in AGENTS.md --- AGENTS.md | 67 +++++++++++++++++++++++++++++++++++++++---------------- 1 file changed, 48 insertions(+), 19 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index 8100aa8..213623d 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -1,33 +1,62 @@ # AGENTS.md -## Purpose - -Lean 4 formalization of quantum systems from an operator-algebraic perspective. -All proofs must be axiom-free: no `sorry` / `admit` / custom `axiom` declarations, -and no mathematical assumptions hidden in structure fields. - ## Project Layout -- `QuantumSystem/Algebra/CStarAlgebra/` — states, GNS, Gelfand–Naimark. May import Mathlib and siblings. - `QuantumSystem/ForMathlib/` — only Mathlib imports allowed; candidates for upstreaming. - `QuantumSystem.lean` — aggregate root that re-exports every module. - `scripts/mk_all.lean` — regenerates the aggregate. -- `lakefile.toml`, `lean-toolchain`, `lake-manifest.json` — **do not edit**. +- `lakefile.toml`, `lean-toolchain`, `lake-manifest.json` — pinned toolchain and manifest. -## Workflow +## Working Principles +**Think before coding.** - Read the target file and its importers before editing. -- Prefer `lean-lsp` MCP tools over shelling out: `lean_goal`, `lean_local_search`, `lean_leansearch`, `lean_loogle`. -- When stuck on a goal: capture it with `lean_goal`, search closing lemmas with `lean_state_search` / `lean_hammer_premise`, then verify with `lean_multi_attempt` before editing. -- If Lean reports `expected '{' or indented tactic sequence`, fix indentation first — almost always a whitespace issue, not a tactic bug. - -## Verification (Definition of Done) - -- A change is done only when `lake build` completes with no new errors or warnings on the edited modules. - **Why:** type-checking an isolated file is not enough; downstream modules can still break. -- After adding imports, run `lean_build` via MCP to restart the LSP; otherwise `lean_diagnostic_messages` suffices. -- If a new top-level module is introduced, regenerate `QuantumSystem.lean` via `scripts/mk_all.lean`. +- State your assumptions about the goal, the existing lemmas, and the proof + skeleton before typing tactics. Capture the goal with `lean_goal` rather + than guessing the shape from the file context. +- Prefer `lean-lsp` MCP tools over shelling out: `lean_goal`, + `lean_local_search`, `lean_leansearch`, `lean_loogle`. If you do not know + whether a lemma exists, say so and search; do not invent plausible-looking + names. +- When stuck on a goal, search closing lemmas with `lean_state_search` / + `lean_hammer_premise`, then verify with `lean_multi_attempt` before + editing. +- If Lean reports `expected '{' or indented tactic sequence`, fix indentation + first — almost always a whitespace issue, not a tactic bug. + **Why:** tactics that compile by accident can mask unsoundness; this + project mandates a fully axiom-free codebase. + +**Simplicity first.** +- Formalize only what the current task requires. No speculative + generalizations, no helper lemmas "for later", no premature abstraction + across `CStarAlgebra` / `StarAlgebra` / `NormedAlgebra`. +- Prefer the most direct proof that closes the goal over the cleverest one. + If `simp` / `linarith` / `aesop` suffices, do not unfold by hand. + **Why:** every extra declaration is surface area to maintain and to keep + axiom-free; speculative API decays faster than it earns interest. + +**Surgical changes.** +- Edit only files demanded by the task. Resist opportunistic renames, + whitespace fixes, or namespace reshuffles in unrelated proofs. +- Do not rewrite existing proofs that already compile. If a proof is ugly + but correct, leave it; flag it in review rather than touching it. + **Why:** Mathlib-style review is line-noise sensitive, and unrelated edits + break `git blame` and inflate merge conflicts. + +**Goal-driven verification (Definition of Done).** +- A change is done only when `lake build` completes with no new errors or + warnings on the edited modules and their downstream importers. +- After adding imports, run `lean_build` via MCP to restart the LSP; + otherwise `lean_diagnostic_messages` suffices. +- If a new top-level module is introduced, regenerate `QuantumSystem.lean` + via `scripts/mk_all.lean`. +- When a tactic fails to close a goal, do not stack `try` / `<;>` to silence + the error — re-inspect the goal with `lean_goal` and address the actual + mismatch. - Never report a task as successful until the above checks pass. + **Why:** "looks right" is not a soundness gate; the kernel is, and + downstream modules can still break even when the edited file type-checks + in isolation. ## Editing Hygiene From 72638076eafbbc63f8390892a751d6e6582a5810 Mon Sep 17 00:00:00 2001 From: suzuki Date: Mon, 4 May 2026 16:57:17 +0000 Subject: [PATCH 2/5] chore: scope references/ ignore to top-level only The `references/` glob also caught documentation directories under each skill (.claude/skills/*/references/). Anchor the rule to the repo root so skill-internal references are tracked. Co-Authored-By: Claude Opus 4.7 (1M context) --- .gitignore | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.gitignore b/.gitignore index 89a592c..b88588e 100644 --- a/.gitignore +++ b/.gitignore @@ -2,7 +2,7 @@ node_modules/ lefthook-local.yml -references/ +/references/ skill-creator-tests/ **/__pycache__/ From cbb94b6851087bc0b98ed1dba0f16a1b4a0b8898 Mon Sep 17 00:00:00 2001 From: suzuki Date: Mon, 4 May 2026 16:57:32 +0000 Subject: [PATCH 3/5] =?UTF-8?q?feat(skills):=20add=20=E2=86=92=20formalize?= =?UTF-8?q?d:=20tier=20and=20filesystem=20issue=20tracker?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Recognise `→ formalized: QuantumSystem.X.y` as a third concept tier above `→ mathlib:` on INDEX.md Key concepts bullets. The same `[UNVERIFIED]` loop in verify_mathlib_refs.py extracts both kinds and tags each worklist item with `kind` (mathlib | formalized). - Add gap-filler/scripts/issues.py with add / list / close subcommands, idempotent on (kind, slug, concept, candidate). `mark-unverified` opens one tracker entry per failure via subprocess so unresolved references survive across sessions; pass --no-issues to suppress. - Document the new tier in pdf-to-knowledge / web-to-knowledge SKILL.md and pdf-to-knowledge/references/output-format.md. Co-Authored-By: Claude Opus 4.7 (1M context) --- .claude/skills/gap-filler/scripts/issues.py | 401 ++++++++++++++++++ .claude/skills/pdf-to-knowledge/SKILL.md | 12 +- .../references/output-format.md | 207 +++++++++ .../scripts/verify_mathlib_refs.py | 210 +++++++-- .claude/skills/web-to-knowledge/SKILL.md | 17 +- 5 files changed, 815 insertions(+), 32 deletions(-) create mode 100644 .claude/skills/gap-filler/scripts/issues.py create mode 100644 .claude/skills/pdf-to-knowledge/references/output-format.md diff --git a/.claude/skills/gap-filler/scripts/issues.py b/.claude/skills/gap-filler/scripts/issues.py new file mode 100644 index 0000000..4c41ef2 --- /dev/null +++ b/.claude/skills/gap-filler/scripts/issues.py @@ -0,0 +1,401 @@ +#!/usr/bin/env python3 +# /// script +# requires-python = ">=3.10" +# dependencies = [] +# /// +"""Lightweight, file-system-based issue tracker for the skills pipeline. + +A counterpart to repoprover's ``issues/*.yaml``: each concern raised by a +script (``[UNVERIFIED]`` mathlib annotation, notation candidate skipped +because of a scope conflict, an open question for the user) lands as a +single YAML file under ``/issues/`` so it survives +across Claude sessions and can be greppable / closeable later. + +Subcommands: + +- ``add`` Create a new issue YAML. Idempotent on + ``(kind, slug, concept, candidate)`` — re-adding a matching + open issue is a no-op so callers can run on every + invocation without flooding the directory. +- ``list`` Print every issue (default: open only) as JSON. +- ``close`` Move a single issue file or every match for a + ``--kind`` / ``--slug`` filter into ``issues/closed/``. + +Issue file schema (plain key/value YAML; nested mappings unsupported): + + opened: 2026-05-04T10:30:00+00:00 + opened_by: verify_mathlib_refs.mark_unverified + kind: unverified-mathlib-ref + slug: araki-1976 + concept: "cyclic vector" + candidate: "Mathlib.Foo.Bar" + reason: "lean_verify did not accept any candidate" + suggested_action: "Re-search or open gap-filler" + status: open + +Usage: + + python3 issues.py add --kind [--slug ...] + [--concept ...] [--candidate ...] + [--reason ...] [--opened-by ...] + [--suggested-action ...] + python3 issues.py list [--kind ...] [--slug ...] + [--include-closed] + python3 issues.py close (--id + | --kind [--slug ...]) + +The script is dependency-free; the YAML it emits is a strict subset that +``parse_issue`` round-trips losslessly. +""" + +from __future__ import annotations + +import argparse +import datetime as _dt +import json +import re +import sys +from pathlib import Path + + +SAFE_FILENAME = re.compile(r"[^A-Za-z0-9._-]+") + + +def _now_iso() -> str: + return _dt.datetime.now(_dt.timezone.utc).isoformat(timespec="seconds") + + +def _safe(token: str, fallback: str = "x") -> str: + """Reduce *token* to filename-safe characters.""" + if not token: + return fallback + out = SAFE_FILENAME.sub("-", token).strip("-") + return out[:50] or fallback + + +def _yaml_quote(value: str) -> str: + """Quote *value* if it contains characters YAML would otherwise misread. + + Conservative: any quote, colon, ``#``, leading/trailing whitespace, or + line break forces double-quoting with the same escape set Python's + ``json.dumps`` uses (``\\n``, ``\\"``, ``\\\\``). + """ + if not value: + return '""' + needs_quote = ( + any(ch in value for ch in ('"', "'", ":", "#", "\n", "\r")) + or value != value.strip() + or value.lower() in {"true", "false", "null", "~"} + ) + if not needs_quote: + return value + escaped = ( + value.replace("\\", "\\\\") + .replace('"', '\\"') + .replace("\n", "\\n") + .replace("\r", "\\r") + ) + return f'"{escaped}"' + + +def _yaml_unquote(raw: str) -> str: + raw = raw.strip() + if (raw.startswith('"') and raw.endswith('"')) or ( + raw.startswith("'") and raw.endswith("'") + ): + body = raw[1:-1] + body = ( + body.replace("\\n", "\n") + .replace("\\r", "\r") + .replace('\\"', '"') + .replace("\\\\", "\\") + ) + return body + return raw + + +# Order of fields when writing — keeps issue files visually consistent so +# diffs are reviewable. +FIELD_ORDER: tuple[str, ...] = ( + "opened", + "opened_by", + "kind", + "slug", + "concept", + "candidate", + "reason", + "suggested_action", + "status", + "closed", + "closed_by", +) + + +def render_issue(payload: dict) -> str: + lines: list[str] = [] + seen: set[str] = set() + for key in FIELD_ORDER: + if key in payload and payload[key] is not None: + lines.append(f"{key}: {_yaml_quote(str(payload[key]))}") + seen.add(key) + for key, value in payload.items(): + if key in seen or value is None: + continue + lines.append(f"{key}: {_yaml_quote(str(value))}") + return "\n".join(lines) + "\n" + + +def parse_issue(text: str) -> dict: + out: dict = {} + for line in text.splitlines(): + if not line.strip() or line.lstrip().startswith("#"): + continue + m = re.match(r"^([A-Za-z_][\w-]*)\s*:\s*(.*)$", line) + if not m: + continue + out[m.group(1)] = _yaml_unquote(m.group(2)) + return out + + +def issues_dir(references_root: Path, *, closed: bool = False) -> Path: + base = references_root / "issues" + return base / "closed" if closed else base + + +def iter_issue_files(references_root: Path, *, include_closed: bool): + base = issues_dir(references_root) + if base.is_dir(): + for entry in sorted(base.iterdir()): + if entry.is_file() and entry.suffix == ".yaml": + yield entry + if include_closed: + closed_dir = issues_dir(references_root, closed=True) + if closed_dir.is_dir(): + for entry in sorted(closed_dir.iterdir()): + if entry.is_file() and entry.suffix == ".yaml": + yield entry + + +def find_open_match( + references_root: Path, + *, + kind: str, + slug: str | None, + concept: str | None, + candidate: str | None, +) -> Path | None: + """Return the first open issue that matches the dedup key, if any.""" + for path in iter_issue_files(references_root, include_closed=False): + try: + payload = parse_issue(path.read_text(encoding="utf-8")) + except OSError: + continue + if payload.get("kind") != kind: + continue + if slug is not None and payload.get("slug") != slug: + continue + if concept is not None and payload.get("concept") != concept: + continue + if candidate is not None and payload.get("candidate") != candidate: + continue + return path + return None + + +def add_issue( + references_root: Path, + *, + kind: str, + slug: str | None, + concept: str | None, + candidate: str | None, + reason: str | None, + suggested_action: str | None, + opened_by: str | None, +) -> dict: + base = issues_dir(references_root) + base.mkdir(parents=True, exist_ok=True) + + existing = find_open_match( + references_root, + kind=kind, + slug=slug, + concept=concept, + candidate=candidate, + ) + if existing is not None: + return {"action": "skip-duplicate", "path": str(existing)} + + timestamp = _dt.datetime.now(_dt.timezone.utc).strftime("%Y%m%dT%H%M%SZ") + name_parts = [timestamp, _safe(kind, fallback="issue")] + if slug: + name_parts.append(_safe(slug)) + if concept: + name_parts.append(_safe(concept)) + filename = "-".join(name_parts) + ".yaml" + path = base / filename + + payload = { + "opened": _now_iso(), + "opened_by": opened_by or "manual", + "kind": kind, + "slug": slug or "", + "concept": concept or "", + "candidate": candidate or "", + "reason": reason or "", + "suggested_action": suggested_action or "", + "status": "open", + } + # Drop empty optional fields so the YAML stays readable. + payload = {k: v for k, v in payload.items() if v != "" or k in ("status",)} + path.write_text(render_issue(payload), encoding="utf-8") + return {"action": "created", "path": str(path)} + + +def list_issues( + references_root: Path, + *, + include_closed: bool, + kind: str | None, + slug: str | None, +) -> list[dict]: + out: list[dict] = [] + for path in iter_issue_files(references_root, include_closed=include_closed): + try: + payload = parse_issue(path.read_text(encoding="utf-8")) + except OSError: + continue + if kind is not None and payload.get("kind") != kind: + continue + if slug is not None and payload.get("slug") != slug: + continue + payload["_path"] = str(path) + payload["_id"] = path.name + out.append(payload) + return out + + +def close_issue( + references_root: Path, + *, + issue_id: str | None, + kind: str | None, + slug: str | None, + closed_by: str | None, +) -> dict: + if issue_id is None and kind is None: + raise ValueError("close: pass --id or --kind to select what to close") + closed_dir = issues_dir(references_root, closed=True) + closed_dir.mkdir(parents=True, exist_ok=True) + moved: list[str] = [] + base = issues_dir(references_root) + if not base.is_dir(): + return {"closed": [], "count": 0} + for path in sorted(base.iterdir()): + if not (path.is_file() and path.suffix == ".yaml"): + continue + if issue_id is not None and path.name != issue_id: + continue + payload = parse_issue(path.read_text(encoding="utf-8")) + if kind is not None and payload.get("kind") != kind: + continue + if slug is not None and payload.get("slug") != slug: + continue + payload["status"] = "closed" + payload["closed"] = _now_iso() + if closed_by: + payload["closed_by"] = closed_by + target = closed_dir / path.name + target.write_text(render_issue(payload), encoding="utf-8") + path.unlink() + moved.append(path.name) + return {"closed": moved, "count": len(moved)} + + +def count_open(references_root: Path) -> int: + base = issues_dir(references_root) + if not base.is_dir(): + return 0 + return sum( + 1 for entry in base.iterdir() if entry.is_file() and entry.suffix == ".yaml" + ) + + +def main() -> int: + parser = argparse.ArgumentParser(description=__doc__) + sub = parser.add_subparsers(dest="cmd", required=True) + + p_add = sub.add_parser("add", help="Create a new issue (idempotent)") + p_add.add_argument("references_root") + p_add.add_argument("--kind", required=True) + p_add.add_argument("--slug", default=None) + p_add.add_argument("--concept", default=None) + p_add.add_argument("--candidate", default=None) + p_add.add_argument("--reason", default=None) + p_add.add_argument("--suggested-action", default=None) + p_add.add_argument("--opened-by", default=None) + + p_list = sub.add_parser("list", help="List issues as JSON") + p_list.add_argument("references_root") + p_list.add_argument("--include-closed", action="store_true") + p_list.add_argument("--kind", default=None) + p_list.add_argument("--slug", default=None) + + p_close = sub.add_parser("close", help="Move open issue(s) into issues/closed/") + p_close.add_argument("references_root") + p_close.add_argument("--id", dest="issue_id", default=None, help="Exact basename") + p_close.add_argument("--kind", default=None) + p_close.add_argument("--slug", default=None) + p_close.add_argument("--closed-by", default=None) + + args = parser.parse_args() + + root = Path(args.references_root).expanduser().resolve() + if not root.is_dir(): + print(f"[error] not a directory: {root}", file=sys.stderr) + return 2 + + if args.cmd == "add": + result = add_issue( + root, + kind=args.kind, + slug=args.slug, + concept=args.concept, + candidate=args.candidate, + reason=args.reason, + suggested_action=args.suggested_action, + opened_by=args.opened_by, + ) + print(json.dumps(result, ensure_ascii=False)) + return 0 + + if args.cmd == "list": + out = list_issues( + root, + include_closed=args.include_closed, + kind=args.kind, + slug=args.slug, + ) + print(json.dumps(out, indent=2, ensure_ascii=False)) + return 0 + + if args.cmd == "close": + try: + result = close_issue( + root, + issue_id=args.issue_id, + kind=args.kind, + slug=args.slug, + closed_by=args.closed_by, + ) + except ValueError as exc: + print(f"[error] {exc}", file=sys.stderr) + return 2 + print(json.dumps(result, indent=2, ensure_ascii=False)) + return 0 + + return 2 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/.claude/skills/pdf-to-knowledge/SKILL.md b/.claude/skills/pdf-to-knowledge/SKILL.md index fa3d623..70a53fd 100644 --- a/.claude/skills/pdf-to-knowledge/SKILL.md +++ b/.claude/skills/pdf-to-knowledge/SKILL.md @@ -105,12 +105,22 @@ about the layout or you need to tweak it). index off this leading identifier, and bullets without one collapse into a `Unnamed concepts` bucket. - Required shape: + Required shape (three tiers, choose the strongest that applies): ```markdown + - `` — → formalized: QuantumSystem.X.y - `` — → mathlib: Mathlib.X.y - `` — → needs formalization ``` + Use `→ formalized: ` only when the concept is already + proven in this repository (`QuantumSystem.*` or another local + module). It outranks `→ mathlib:` because a local proof is + stronger evidence than a mathlib match — `gap-filler` + consequently treats these as the highest tier (`formalized` > + `resolved` > `partial` > `gap`). The tier is verified by the + same `verify_mathlib_refs.py` loop as `mathlib`, so a stale + identifier picks up `[UNVERIFIED]` automatically. + Contents of the bullets: - For **code-adjacent papers**: function/type names, CLI flags, config keys, environment variables, error messages, protocol fields. diff --git a/.claude/skills/pdf-to-knowledge/references/output-format.md b/.claude/skills/pdf-to-knowledge/references/output-format.md new file mode 100644 index 0000000..7f2995c --- /dev/null +++ b/.claude/skills/pdf-to-knowledge/references/output-format.md @@ -0,0 +1,207 @@ +# Output format: `references//` + +Detailed specification of what the skill writes to disk. Read this when you +need to tweak the converter or answer a user question about where something +lives. + +## Directory layout + +``` +references// +├── INDEX.md +├── content.md (page count <= 20, OR > 20 but no H1 headings to split on) +├── sections/ (page count > 20 and the PDF has H1 headings) +│ ├── 01-.md +│ └── 02-.md +├── assets/ +│ ├── image_000001_.jpg +│ └── image_000002_.jpg +└── mineru-raw/ (only with --keep-raw; see the last section for contents) +``` + +Exactly one of `content.md` or `sections/` exists — never both. Keeps the +agent's mental model simple. + +## Slug derivation + +- arXiv URLs (`arxiv.org/abs/2501.12345v1`, `arxiv.org/pdf/2501.12345`) → + `arxiv-2501.12345`. Version suffix is stripped so re-fetching v2 lands in + the same directory. +- Other URLs → slugified filename from the URL path (`.pdf` stripped). +- Local paths → slugified basename. +- `--slug` flag always wins. + +## `INDEX.md` structure + +```markdown +--- +title: "..." +source: "" +pages: +slug: +assets: # number of extracted image files +authors: ["Name1", "Name2"] # populated by Claude in step 4a; omitted if unknown +bibliography: # populated by Claude in step 4e; empty list if the paper has no References + - key: "" + title: "" + authors: ["Name1", ...] + venue: "" + year: + arxiv: "" + doi: "" + ingested: false # true when the referenced paper is already under references/; used by the concept index +--- + +# + +## Summary +<!-- 3-5 sentences, filled in by Claude after conversion --> + +## Key concepts +<!-- bullet list of identifiers; deleted entirely if not applicable. + Each bullet may end with a tier annotation: + - `<term>` — definition/description → formalized: `QuantumSystem.A.b` + - `<term>` — definition/description → mathlib: `Mathlib.A.B.c` + - `<term>` — definition/description → needs formalization +--> + +## Contents +- [<section title>](sections/NN-<slug>.md) +- ... +``` + +Frontmatter is plain YAML — machine-readable. The body is human/agent-readable +navigation. Summary and Key concepts are scaffolded as `<!-- TODO -->` blocks; +Claude replaces them. `authors` is filled by Claude after scanning the first +page of `content.md`; when present it powers author-name-based related-work +search in step 4d. `bibliography` is populated in step 4e and drives the +cross-document "next papers to ingest" suggestions (currently manual, +automated in a future iteration). + +### Concept annotations + +Cross-references live inline on each Key concepts bullet as a trailing +arrow annotation. Three forms are recognised by `update_concepts.py`, +`detect_gaps.py`, and `verify_mathlib_refs.py`: + +- `→ formalized: QuantumSystem.X.y` — locally proven in this repository. + Strongest tier; outranks `resolved` for prioritisation. +- `→ mathlib: Mathlib.X.y` — present in mathlib (term or author search hit + that passed `lean_verify`). Tier `resolved`. +- `→ needs formalization` — no match in either search axis. Tier `gap`. + +A `[UNVERIFIED] (reason)` suffix is appended by +`verify_mathlib_refs.py mark-unverified` when the candidate failed +`lean_verify`; both `mathlib` and `formalized` annotations participate in +that loop. + +They are plain Markdown — agents can `grep -n "→ formalized:"`, +`grep -n "→ mathlib:"`, `grep -n "→ needs formalization"`, or +`grep -n "[UNVERIFIED]"` to slice an INDEX.md by tier. The annotation is +added only when the session has Lean MCP tooling; otherwise it is +omitted. + +### ToC detail + +- **Split mode (sections/)**: one entry per section file in document order. +- **Monolith mode (content.md)**: the "Full content" link, followed by + indented child links for each H2/H3 heading (up to 20) with GitHub-style + anchor fragments — e.g. ``[3 Model Architecture](content.md#3-model-architecture)``. + This lets an agent jump straight to the relevant section without scanning + the whole file. + +## Section splitting rules + +Trigger: `page_count > --max-pages-per-section` (default 20). + +Algorithm: +1. Walk the raw Markdown line by line. +2. Each `# ` line starts a new section. `## `, `### `, etc. are body. +3. Content before the first `# ` (if non-empty) becomes a `front-matter` + section, numbered first. +4. If only one real section is produced, fall back to a single `content.md` + (no splitting, ToC points at the monolith). + +Section filenames are `NN-<heading-slug>.md` where `NN` is a zero-padded +1-based index and the slug is derived the same way as the top-level slug +(lowercase, ASCII-ish, max 60 chars). + +## Image handling + +- MinerU writes extracted images into `<scratch>/<name>/auto/images/` with + hash-named JPG files and references them from the Markdown as + `images/<hash>.jpg`. The post-processor in `scripts/convert.py` rewrites + these references to `assets/<hash>.jpg`, copies **only the referenced** + images into `assets/`, and drops any orphan clips MinerU may have left + behind (mostly per-formula crops MinerU keeps as debugging spare data). +- For pure math papers with no figures MinerU's `images/` directory still + gets populated with formula clips. None of them are referenced from the + Markdown (LaTeX handles the equations), so `assets/` ends up empty — the + converter does not create it in that case. + +## Formulas + +Always on. MinerU emits LaTeX for both inline (`$...$`) and display (`$$...$$`) +math. Equation numbering is preserved via `\tag{...}`. No opt-in flag is +needed; the formula recogniser runs as part of the `pipeline` backend at +modest additional CPU cost (~2 minutes on an 18-page paper). + +## OCR + +Off by default (`--ocr` to enable). Running OCR on a text-native PDF is slow +and often introduces transcription errors. Switch MinerU's method to `ocr` +only when the user confirms the PDF is scanned or when the initial +conversion returned near-empty Markdown. + +## `CONCEPTS.md` (cross-document index) + +Sibling of the per-slug subdirs under `references/`. Regenerated by +`scripts/update_concepts.py` at the end of step 4f in the workflow. + +``` +references/ +├── CONCEPTS.md # this file +├── arxiv-2202.03357/ +│ └── INDEX.md +├── arxiv-1706.03762/ +│ └── INDEX.md +└── ... +``` + +Content: + +```markdown +# Concepts index + +Auto-generated from references/*/INDEX.md. Do not edit by hand — rerun +`.claude/skills/pdf-to-knowledge/scripts/update_concepts.py references/`. + +## <Concept title> + +- [<slug>](<slug>/INDEX.md) — <description from Key concepts bullet> → mathlib: Mathlib.A.B.c +- [<another slug>](<another slug>/INDEX.md) — <description> → needs formalization +``` + +Each section header is a concept title (the backtick-quoted identifier at +the head of a `Key concepts` bullet). Entries are grouped by concept so a +glance reveals which papers cover each term and whether any of them gives +a mathlib mapping. The file is fully derived — editing it by hand is +overwritten on the next rebuild. + +Implementation note: concept keys are normalised to lowercase for +deduplication but displayed in their original case. Bullets with no +backtick-quoted lead identifier fall under a synthetic +"`Unnamed concepts`" heading to avoid silent loss. + +## `mineru-raw/` (optional debug artefacts) + +- **Off by default** since iteration-6; pass `--keep-raw` to the converter + to retain them. When enabled, `<slug>/mineru-raw/` holds MinerU's + auxiliary outputs: + - `<name>_middle.json` — raw DocumentAnalysis JSON (2+ MB) + - `<name>_content_list.json` and `_v2` — per-span structured content + - `<name>_model.json` — layout model outputs + - `<name>_layout.pdf`, `_span.pdf`, `_origin.pdf` — annotated PDFs useful + when triaging a conversion bug +- Not intended for agents to `Read`; the useful signal is already in + `content.md` / `INDEX.md`. Safe to delete. diff --git a/.claude/skills/pdf-to-knowledge/scripts/verify_mathlib_refs.py b/.claude/skills/pdf-to-knowledge/scripts/verify_mathlib_refs.py index 261c5e9..6920f42 100644 --- a/.claude/skills/pdf-to-knowledge/scripts/verify_mathlib_refs.py +++ b/.claude/skills/pdf-to-knowledge/scripts/verify_mathlib_refs.py @@ -3,26 +3,30 @@ # requires-python = ">=3.10" # dependencies = [] # /// -r"""Audit ``→ mathlib: ...`` annotations in ``references/*/INDEX.md`` files. +r"""Audit ``→ mathlib: ...`` and ``→ formalized: ...`` annotations. This script does not itself call the Lean toolchain — the actual existence check is performed by the caller (Claude) via the ``mcp__lean-lsp__lean_verify`` MCP tool, one symbol at a time. The script is the mechanical half: -- ``extract`` Walk the references root, pull every ``→ mathlib: ...`` - annotation into a JSON worklist. The caller feeds each - candidate symbol to ``lean_verify`` and records failures - in a ``failed.json``. +- ``extract`` Walk the references root, pull every ``→ mathlib: ...`` and + ``→ formalized: ...`` annotation into a JSON worklist + (each item carries a ``kind`` field discriminating the + two). The caller feeds each candidate symbol to + ``lean_verify`` and records failures in a ``failed.json``. - ``mark-unverified`` Given the caller's ``failed.json``, rewrite each offending INDEX.md bullet so the annotation becomes - ``→ mathlib: \`<path>\` [UNVERIFIED]`` — a marker that + ``→ mathlib: \`<path>\` [UNVERIFIED]`` (or + ``→ formalized: \`<path>\` [UNVERIFIED]``) — a marker that ``gap-filler``'s ``detect_gaps.py`` reads as ``suspect`` status. Rationale: we do not want to trust Claude's judgement on whether a Lean declaration exists. The T1-A remediation is to externalise verification -to the Lean MCP and mark anything that can not be proven to exist. +to the Lean MCP and mark anything that can not be proven to exist. The +same loop applies to ``→ formalized:`` — local declarations rot when +files are renamed, so verifying them on every ingestion catches drift. Usage: python3 verify_mathlib_refs.py extract <references-root> [--output worklist.json] @@ -47,14 +51,29 @@ import datetime as _dt import json import re +import subprocess import sys from pathlib import Path +# Path to the sibling skill's ``issues.py`` (gap-filler owns the tracker +# format; this script is its biggest auto-producer). The lookup is +# best-effort: if the file is missing we silently skip issue creation so +# the verification cycle still works on a partial install. +_ISSUES_SCRIPT = ( + Path(__file__).resolve().parents[2] / "gap-filler" / "scripts" / "issues.py" +) + + KEY_CONCEPTS_HEADER = re.compile(r"^##\s+Key concepts\s*$", re.IGNORECASE) NEXT_H2 = re.compile(r"^##\s+") BULLET = re.compile(r"^\s*-\s+(.*)$") -ANNOT_SPLIT = re.compile(r"(\s*→\s*mathlib\s*:\s*)", re.IGNORECASE) +# Splits a bullet body around a ``→ mathlib:`` or ``→ formalized:`` marker. +# Group 2 captures which kind matched so each worklist item carries a +# ``kind`` field (``mathlib`` vs ``formalized``). +ANNOT_SPLIT = re.compile( + r"(\s*→\s*(mathlib|formalized)\s*:\s*)", re.IGNORECASE +) TICKED = re.compile(r"`([^`]+)`") UNVERIFIED_MARKER = "[UNVERIFIED]" VERIFIED_FIELD = "mathlib_verified" @@ -151,13 +170,16 @@ def extract(root: Path) -> dict: if not body or body.startswith("<!--"): continue parts = ANNOT_SPLIT.split(body, maxsplit=1) - if len(parts) < 3: + # ANNOT_SPLIT has two capture groups: ``(full_marker, kind)`` — + # so ``re.split`` returns ``[before, full_marker, kind, after]``. + if len(parts) < 4: continue - annotation = parts[1] + parts[2] + full_marker, kind, after = parts[1], parts[2].lower(), parts[3] + annotation = full_marker + after if UNVERIFIED_MARKER in annotation: continue # already flagged; leave alone concept = _extract_concept_name(body) - candidates = _collect_candidates(parts[2], concept) + candidates = _collect_candidates(after, concept) if not candidates: continue items.append( @@ -165,6 +187,7 @@ def extract(root: Path) -> dict: "slug": slug, "index_path": str(index_path), "line": idx, + "kind": kind, "concept": concept, "raw_annotation": annotation.strip(), "candidates": candidates, @@ -228,17 +251,51 @@ def _read_frontmatter_field(index_path: Path, field: str) -> str | None: return None -def _mark_one(index_path: Path, line_no: int, reason: str, *, dry_run: bool) -> bool: +def _bullet_metadata(line: str) -> dict: + """Extract the kind / concept / candidate visible on a Key concepts bullet.""" + info = {"kind": "mathlib", "concept": "", "candidate": ""} + m_kind = re.search( + r"→\s*(formalized|mathlib)\s*:\s*(.*)$", line, re.IGNORECASE + ) + if m_kind: + info["kind"] = m_kind.group(1).lower() + # First backticked or qualified token after the marker is the + # candidate the verifier rejected. + tail = m_kind.group(2) + m_tick = re.search(r"`([^`]+)`", tail) + if m_tick: + info["candidate"] = m_tick.group(1).strip() + else: + m_bare = re.search(r"[A-Za-z_][\w.]+", tail) + if m_bare: + info["candidate"] = m_bare.group(0).strip() + m_concept = re.search(r"`([^`]+)`", line) + if m_concept: + info["concept"] = m_concept.group(1).strip() + return info + + +def _mark_one( + index_path: Path, line_no: int, reason: str, *, dry_run: bool +) -> dict | None: + """Patch the bullet at *line_no* with ``[UNVERIFIED]``. + + Returns ``None`` if no patch was applied (out-of-range or already + flagged). Otherwise returns a record carrying the bullet's + ``kind`` / ``concept`` / ``candidate`` metadata so the caller can + open a matching tracker issue. + """ text = index_path.read_text(encoding="utf-8", errors="replace") lines = text.splitlines(keepends=True) if line_no < 1 or line_no > len(lines): print(f"[warn] out-of-range line {line_no} in {index_path}", file=sys.stderr) - return False + return None original = lines[line_no - 1] if UNVERIFIED_MARKER in original: - return False # nothing to do + return None # nothing to do had_trailing_nl = original.endswith("\n") stripped = original.rstrip("\n") + metadata = _bullet_metadata(stripped) # Append the marker at the very end of the bullet; reason optional. if reason: patched = f"{stripped} {UNVERIFIED_MARKER} ({reason})" @@ -247,30 +304,117 @@ def _mark_one(index_path: Path, line_no: int, reason: str, *, dry_run: bool) -> lines[line_no - 1] = patched + ("\n" if had_trailing_nl else "") if dry_run: print(f"[dry-run] {index_path}:{line_no}: {stripped!r} -> {patched!r}") - return True + return metadata index_path.write_text("".join(lines), encoding="utf-8") - return True + return metadata + + +def _open_issue_for_failure( + references_root: Path, + *, + slug: str, + metadata: dict, + reason: str, +) -> dict | None: + """Best-effort issue creation via the sibling ``issues.py`` CLI. + + Returns the parsed JSON output of ``issues.py add`` on success, or + ``None`` when the script is unavailable (partial install) or the + invocation fails. + """ + if not _ISSUES_SCRIPT.is_file(): + return None + kind = "unverified-formalized-ref" if metadata.get("kind") == "formalized" else "unverified-mathlib-ref" + cmd = [ + sys.executable, + str(_ISSUES_SCRIPT), + "add", + str(references_root), + "--kind", + kind, + "--opened-by", + "verify_mathlib_refs.mark_unverified", + ] + if slug: + cmd += ["--slug", slug] + if metadata.get("concept"): + cmd += ["--concept", metadata["concept"]] + if metadata.get("candidate"): + cmd += ["--candidate", metadata["candidate"]] + if reason: + cmd += ["--reason", reason] + cmd += [ + "--suggested-action", + "Re-search a candidate or open gap-filler to ingest a better source.", + ] + try: + result = subprocess.run( + cmd, capture_output=True, text=True, check=True, timeout=15 + ) + except (subprocess.SubprocessError, OSError) as exc: + print(f"[warn] issues.py add failed for {slug}: {exc}", file=sys.stderr) + return None + out = result.stdout.strip() + try: + return json.loads(out) if out else None + except json.JSONDecodeError: + return None -def mark_unverified(root: Path, failures: list[dict], *, dry_run: bool) -> dict: +def mark_unverified( + root: Path, failures: list[dict], *, dry_run: bool, create_issues: bool = True +) -> dict: marked = 0 skipped = 0 per_slug: dict[str, list[int]] = {} - for failure in failures: - slug = failure.get("slug") - line_no = failure.get("line") - reason = (failure.get("reason") or "").strip() - if not slug or not line_no: + issues_opened: list[dict] = [] + for idx, failure in enumerate(failures, start=1): + if not isinstance(failure, dict): + print(f"[warn] failure #{idx} is not an object", file=sys.stderr) skipped += 1 continue + slug_raw = failure.get("slug") + if not isinstance(slug_raw, str) or not slug_raw.strip(): + print(f"[warn] failure #{idx} has no usable slug", file=sys.stderr) + skipped += 1 + continue + slug = slug_raw.strip() + line_raw = failure.get("line") + try: + if isinstance(line_raw, bool): + raise ValueError + line_no = int(line_raw) + except (TypeError, ValueError): + print( + f"[warn] failure #{idx} has invalid line {line_raw!r}", + file=sys.stderr, + ) + skipped += 1 + continue + if line_no < 1: + print( + f"[warn] failure #{idx} has out-of-range line {line_no}", + file=sys.stderr, + ) + skipped += 1 + continue + reason_raw = failure.get("reason") + reason = reason_raw.strip() if isinstance(reason_raw, str) else "" index_path = root / slug / "INDEX.md" if not index_path.is_file(): print(f"[warn] missing INDEX.md for slug {slug!r}", file=sys.stderr) skipped += 1 continue - if _mark_one(index_path, int(line_no), reason, dry_run=dry_run): + metadata = _mark_one(index_path, line_no, reason, dry_run=dry_run) + if metadata is not None: marked += 1 - per_slug.setdefault(slug, []).append(int(line_no)) + per_slug.setdefault(slug, []).append(line_no) + if create_issues and not dry_run: + opened = _open_issue_for_failure( + root, slug=slug, metadata=metadata, reason=reason + ) + if opened: + issues_opened.append({"slug": slug, **opened}) else: skipped += 1 # After patching (real mode), stamp every INDEX.md with a fresh @@ -288,6 +432,7 @@ def mark_unverified(root: Path, failures: list[dict], *, dry_run: bool) -> dict: "per_slug": per_slug, "dry_run": dry_run, "stamped_slugs": stamped, + "issues_opened": issues_opened, } @@ -356,6 +501,16 @@ def main() -> int: p_mark.add_argument("references_root") p_mark.add_argument("--from", dest="failures_path", required=True) p_mark.add_argument("--dry-run", action="store_true") + p_mark.add_argument( + "--no-issues", + action="store_true", + help=( + "Suppress automatic issue creation under <root>/issues/. By " + "default each newly stamped [UNVERIFIED] bullet opens an " + "idempotent tracker entry so the false positive is not " + "forgotten across sessions." + ), + ) p_check = sub.add_parser( "check-done", @@ -393,7 +548,12 @@ def main() -> int: if not isinstance(failures, list): print("[error] failures JSON must be a list of objects", file=sys.stderr) return 2 - summary = mark_unverified(root, failures, dry_run=args.dry_run) + summary = mark_unverified( + root, + failures, + dry_run=args.dry_run, + create_issues=not args.no_issues, + ) print(json.dumps(summary, indent=2, ensure_ascii=False)) return 0 diff --git a/.claude/skills/web-to-knowledge/SKILL.md b/.claude/skills/web-to-knowledge/SKILL.md index 4a379c9..2531f73 100644 --- a/.claude/skills/web-to-knowledge/SKILL.md +++ b/.claude/skills/web-to-knowledge/SKILL.md @@ -96,12 +96,17 @@ Full format spec: `references/output-format.md`. ``` or a single paragraph. Skip if the page has no meaningful outbound links. - d. **Mathlib cross-reference** — same technique as `pdf-to-knowledge` - step 4d. For each Key concepts bullet, run - `lean_local_search <term>` plus `lean_local_search <author-name>` for - names that appear prominently in the page. Annotate matches with - `→ mathlib: Mathlib.X.y`, misses with `→ needs formalization`. Skip - entirely if the Lean MCP toolchain is unavailable. + d. **Mathlib / local cross-reference** — same technique as + `pdf-to-knowledge` step 4d. For each Key concepts bullet, pick the + strongest tier that applies: + + - `→ formalized: QuantumSystem.X.y` if the concept is already proven + locally in this repository (verified via `lean_verify`). + - `→ mathlib: Mathlib.X.y` if a `lean_local_search <term>` or + `lean_local_search <author-name>` hit verifies cleanly. + - `→ needs formalization` if both searches miss. + + Skip entirely if the Lean MCP toolchain is unavailable. **Every annotation must pass through the step-6 verification loop** — do not trust `lean_local_search` hits at face value. From d0ccc88da3845907dff803d9a159c49b3c2641f7 Mon Sep 17 00:00:00 2001 From: suzuki <casek2703@gmail.com> Date: Mon, 4 May 2026 16:57:50 +0000 Subject: [PATCH 4/5] feat(skills/gap-filler): align goal coverage with Lean declarations MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Earlier goals.yaml measured satisfaction via `concepts` matched against INDEX.md bullets — a knowledge-coverage proxy, not real Lean verification. Switch the truth source to `declarations`, scanned directly from <lean-root>/**/*.lean. - detect_gaps.py: bespoke YAML subset parser (block + flow `{}` / `[]`); Lean scanner that tracks namespace / end stacks to build fully-qualified declaration names; hard validation on malformed goals.yaml; new --lean-root, --history-log, --no-history flags; gaps-history.jsonl now records declarations_total / declarations_verified. - New goals.yaml schema: `declarations: [Lean.Path.foo]` is the truth; `concepts: [bare-string | {name, sources: [{slug, anchor: {kind: ref}}]}]` is informational hint for gap-filler. Coverage = verified_decls / total_decls; an empty `declarations: []` slot counts as one missing target so TODOs do not silently inflate the score. - Populate goals.yaml at the repo root with the 7 README highlights plus the abstract-local-net SSA TODO; the scanner verifies 19/20 declarations against the current QuantumSystem tree (score 0.95). - Update gap-filler SKILL.md "Side channels" and references/ workflow.md with the new schema and worked examples. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --- .claude/skills/gap-filler/SKILL.md | 182 +++- .../skills/gap-filler/references/workflow.md | 336 +++++++ .../skills/gap-filler/scripts/detect_gaps.py | 942 +++++++++++++++++- goals.yaml | 120 +++ 4 files changed, 1522 insertions(+), 58 deletions(-) create mode 100644 .claude/skills/gap-filler/references/workflow.md create mode 100644 goals.yaml diff --git a/.claude/skills/gap-filler/SKILL.md b/.claude/skills/gap-filler/SKILL.md index b993d64..8ac64a3 100644 --- a/.claude/skills/gap-filler/SKILL.md +++ b/.claude/skills/gap-filler/SKILL.md @@ -5,9 +5,9 @@ description: Recursively expand `references/` to cover the prerequisites of a fo # gap-filler -Turn a formalization goal into a bounded recursive ingestion plan, then -execute it. Orchestrates the existing `pdf-to-knowledge` and -`web-to-knowledge` skills. +Turn a formalization goal into a bounded recursive ingestion plan and, +with user approval, execute it. Orchestrates the existing +`pdf-to-knowledge` and `web-to-knowledge` skills. ## When to invoke @@ -55,8 +55,22 @@ commit if you want audit history, or to `.gitignore` for ephemeral runs. python3 .claude/skills/gap-filler/scripts/detect_gaps.py \ references/ --target-slug <target-slug> --output references/gaps.json ``` + + When the project has a `goals.yaml` (a fixed list of formalization + targets — see "Side channels" below), pass + `--goals goals.yaml --lean-root <Lean tree>` so the report adds + per-goal status verified against the actual Lean declarations, plus + `goal_coverage_score = verified_declarations / total_declarations`. + The plain `coverage_score` keeps its meaning ("ingestion-wide + knowledge coverage"); use whichever the user asked for. Both can + appear in the same report. The report lists every Key concepts bullet's status across all ingested slugs: + - `formalized` — at least one source annotated + `→ formalized: QuantumSystem.X.y` (a local proof in this repo) and + `verify_mathlib_refs.py` did not flag it. Strongest tier; outranks + `resolved` because a local proof is harder evidence than a mathlib + match. - `resolved` — at least one source annotated `→ mathlib: ...` and `verify_mathlib_refs.py` did not flag it as `[UNVERIFIED]`. - `suspect` — a source annotated `→ mathlib: ...` but @@ -76,7 +90,18 @@ commit if you want audit history, or to `.gitignore` for ephemeral runs. - `ambiguous` — no annotation (rarely happens if previous ingestions followed the SKILL.md contract). - `other_knowledge` — concepts coming from non-target slugs (may - still be useful prerequisites). + still be useful prerequisites). Its `status` field uses the + strongest available source-tier vocabulary (`formalized`, + `resolved`, `suspect`, `gap`, or `ambiguous`), including `suspect` + when the only known annotation is an `[UNVERIFIED]` false positive. + + When `--goals` is enabled, the goal block introduces two more status + vocabularies: + - goal-concept `status` may also be `unknown` — the concept was + pinned to specific `sources[*].slug` entries, but none of those + slugs currently document it. + - goal `goal_status` is one of `satisfied`, `partially_satisfied`, + `missing`, or `unverified`. Concept-name matching is normalised aggressively: `Connes cocycle`, `Connes.cocycle`, `ConnesCocycle`, and `connes-cocycle` all merge. @@ -84,11 +109,12 @@ commit if you want audit history, or to `.gitignore` for ephemeral runs. then lowercased and punctuation-stripped. The report also exposes `coverage_score`, a single 0..1 number - equal to `(resolved × 1.0 + partial × 0.5) / target_total`. Use - this as the headline progress metric when reporting to the user — - it captures "real mathlib coverage plus local-reference coverage" - in one figure, so an ingestion that adds 3 Wikipedia pages moves - the number even when `resolved` stays flat. + equal to + `(formalized × 1.0 + resolved × 1.0 + partial × 0.5) / target_total`. + Use this as the headline progress metric when reporting to the user — + it captures "local proof + mathlib coverage + local-reference + coverage" in one figure, so an ingestion that adds 3 Wikipedia pages + moves the number even when `formalized` and `resolved` stay flat. 3. **Rank the target's bibliography by centrality.** ```bash @@ -102,23 +128,11 @@ commit if you want audit history, or to `.gitignore` for ephemeral runs. For each **uninvested entry without arxiv / DOI** — the common case for operator algebra, older physics and pre-2000 math — the script - also emits `suggested_search_queries`. The order depends on the - entry's publication year: - - - ``year >= 1995``: university-domain PDF rotation first - (`caltech.edu`, `mit.edu`, `math.berkeley.edu`, `cam.ac.uk`, - `ihes.fr`, `kurims.kyoto-u.ac.jp`, ...), then `lecture-notes`, - then `nlab` / `wikipedia`. Matches the iter-2 win of Jones's - 2009 Berkeley lecture notes. - - ``year < 1995``: `lecture-notes` leads, followed by NUMDAM / - Project Euclid / open-access-pdf fallbacks, with university - domains demoted to the tail. The iter-2 eval found that 3 - university domains × 2 legacy entries (PP86, Kos86a) drew zero - useful hits while `"lecture notes" filetype:pdf` surfaced - NUMDAM's OA host of PP86 and Carlen's AZ-school notes for - Kos86a. - - See step 4 for how to consume the queries. + also emits `suggested_search_queries`. The ordering switches on + publication year (`year >= 1995` favours university-domain PDFs; + `year < 1995` favours `lecture-notes` + NUMDAM / Project Euclid). + See [./references/workflow.md](./references/workflow.md) for the + calibration story and a concrete sample of the emitted queries. 4. **Synthesise a plan.** Read both JSON files and compose a **short ingestion plan**: @@ -127,19 +141,16 @@ commit if you want audit history, or to `.gitignore` for ephemeral runs. 1. **arxiv / DOI in the bibliography** — top of the ranked list with a discoverable URL → `pdf-to-knowledge`. - 2. **University lecture-notes PDF** — when the bibliography entry - has no arxiv ID but the topic is covered in standard graduate - curricula (subfactor theory, modular theory, KMS states, - entropy inequalities). Use the `suggested_search_queries` - emitted by `rank_bibliography.py`: feed them to `WebSearch`, - pick the most reputable PDF hit (faculty page > course page - > personal blog), hand the URL to `pdf-to-knowledge`. - **Why this usually beats Wikipedia**: lecture notes are - written by a single modern author with a coherent narrative, - whereas Wikipedia articles on advanced operator-algebraic - topics are often stubs or written by different editors with - mismatched notation. Do not skip this step for math-heavy - gaps. + 2. **University lecture-notes PDF** — when the entry has no arxiv + ID but the topic is covered in standard graduate curricula + (subfactor theory, modular theory, KMS states, entropy + inequalities). Feed the `suggested_search_queries` to + `WebSearch`, pick the most reputable PDF hit (faculty page > + course page > personal blog), hand it to `pdf-to-knowledge`. + For math-heavy gaps lecture notes usually beat Wikipedia + (single author, coherent notation); see + [./references/workflow.md](./references/workflow.md) for the + comparison. 3. **Wikipedia / nLab** — good for broadly-known math (`Von_Neumann_entropy`, `Tomita–Takesaki_theory`) and as a zero-effort fallback when the lecture-notes search returns @@ -158,6 +169,12 @@ commit if you want audit history, or to `.gitignore` for ephemeral runs. 5. **Execute (with user OK).** For each approved entry in the plan: - If the source is an arxiv ID: invoke `pdf-to-knowledge` with `https://arxiv.org/pdf/<id>`. + - If the source is a DOI with a direct open PDF URL, or an open-access + publisher PDF URL discovered from that DOI: invoke `pdf-to-knowledge` + with the PDF URL. If only a DOI landing page is available, ask before + using a weaker HTML fallback. + - If the source is a discovered university / course / faculty PDF URL: + invoke `pdf-to-knowledge` with that PDF URL. - If the source is a Wikipedia / nLab URL: invoke `web-to-knowledge` with that URL. - After **each** ingestion, re-run @@ -170,6 +187,85 @@ commit if you want audit history, or to `.gitignore` for ephemeral runs. Do not loop automatically — hand control back to the user and wait for them to approve another round. +## Side channels + +Three optional outputs that complement `gaps.json`. Every one has a +worked example in [./references/workflow.md](./references/workflow.md); +the summary below gives just the contract. + +- **`references/gaps-history.jsonl`** — append-only JSONL, one record per + `detect_gaps.py` run with `timestamp / coverage_score / + goal_coverage_score / counts / issues_open`. Use it to attribute + progress to specific ingestions. `--no-history` suppresses; + `--history-log <path>` redirects. + +- **`references/issues/*.yaml`** — file-system tracker for items the + pipeline could not auto-resolve (`[UNVERIFIED]` mathlib refs, skipped + notation candidates, open questions). `verify_mathlib_refs.py + mark-unverified` opens these automatically (idempotent on + `kind + slug + concept + candidate`); manual ones go through + `scripts/issues.py {add,list,close}`. `detect_gaps.py` reports + `issues.open` in its summary. + +- **`goals.yaml`** (project root, checked into git) — pins the + formalization targets so the headline metric tracks "what we promised + to prove", not "what we happened to ingest". Pass + `--goals goals.yaml --lean-root <Lean tree>` to `detect_gaps.py`. + + **Truth source = `declarations`.** Each goal lists fully-qualified + Lean declaration names (`Matrix.vonNeumannEntropy_nonneg`, + `gelfand_naimark_theorem`, …). The script walks `<lean-root>/**/*.lean`, + builds the set of every `theorem`/`def`/`structure`/`class`/ + `instance`/`inductive`/`abbrev`/`axiom` (tracking `namespace`/`end` + stacks), and compares. Verified ⇒ goal counted toward + `goal_coverage_score`. Without `--lean-root`, declarations are + reported as `unverified` (no guess). + + Malformed goal entries are a hard error, not a soft fallback: missing + `id` / `description`, non-list `declarations` / `concepts`, or a + structured `sources:` entry without a `slug` makes `detect_gaps.py` + exit 2 with an `[error] invalid goals file: ...` message. + + **`concepts` is informational** — prerequisite knowledge hints used + by `gap-filler`'s plan output, not by the satisfaction judgement. A + concept may be a bare string (any INDEX.md mentioning it counts) or + a structured entry pinning the prerequisite to specific slugs and + optional anchors: + + ```yaml + goals: + - id: gns-construction + description: "Cyclic representation π_ω …" + declarations: + - GNS.Representation + - GNS.Construction.isFaithful_iff_separating + concepts: + - GNS representation # bare string + - name: Tomita-Takesaki modular operator # structured + sources: + - { slug: arxiv-2507.00900, anchor: { theorem: "2.3" } } + - { slug: "92737", anchor: { definition: "modular operator" } } + + - id: ssa-abstract-local-net + description: "TODO." + declarations: [] # → counts as 1 missing + concepts: + - name: localNet + sources: + - { slug: "92737" } + ``` + + `anchor` is a single-key map keyed by the locator kind + (`chapter` / `section` / `subsection` / `theorem` / `definition` / + `lemma` / `proposition` / `corollary` / `equation` / `page` / + `example`). It is human-readable navigation; the matcher only uses + `slug` for filtering. + + **Coverage formula.** `goal_coverage_score = + verified_declarations / total_declarations`, where a goal with + `declarations: []` contributes 1 to the denominator (an unfulfilled + TODO slot, so the score does not silently inflate). + ## Why this design - **Bounded, user-visible plan.** Gap-filling has blast radius (each @@ -194,7 +290,7 @@ commit if you want audit history, or to `.gitignore` for ephemeral runs. their own dependencies in place. This skill does not re-implement their work. - **`uv`** on PATH (same reason as the sibling skills). -- No other Python deps — the two scripts here use stdlib only. +- No other Python deps — the scripts here use stdlib only. ## Failure modes to watch for @@ -212,6 +308,6 @@ commit if you want audit history, or to `.gitignore` for ephemeral runs. goal string with no matching slug, instruct them to run `pdf-to-knowledge` on a primary source first, then come back here. -See `references/workflow.md` for a worked example on the Araki -relative-entropy paper, including the expected `gaps.json` output and a -sample 3-step ingestion plan. +See [./references/workflow.md](./references/workflow.md) for a worked +example on the Araki relative-entropy paper, including the expected +`gaps.json` output and a sample 3-step ingestion plan. diff --git a/.claude/skills/gap-filler/references/workflow.md b/.claude/skills/gap-filler/references/workflow.md new file mode 100644 index 0000000..e1ea785 --- /dev/null +++ b/.claude/skills/gap-filler/references/workflow.md @@ -0,0 +1,336 @@ +# gap-filler workflow — worked example + +Concrete trace of running the skill on the Araki / Longo-Witten paper +(`arxiv-2202.03357`) from `references/` in this project. Use this as a +reference when you need to calibrate expectations against the synthetic +behaviour described in `SKILL.md`. + +## Starting state + +``` +references/ +├── CONCEPTS.md # aggregated concept index +├── arxiv-2202.03357/ +│ ├── INDEX.md # Longo–Witten "A note on continuous entropy" +│ ├── content.md # MinerU output with 184 LaTeX spans +│ └── assets/ # empty (no figures) +``` + +INDEX.md has 14–22 Key concepts bullets (varies across iterations) and a +bibliography of ~24 entries with author-year keys (Ara76, Kos86a, Tak03, +Wit21, …). + +## 0. Optional: pin formalization targets (`goals.yaml`) + +Without a goals file, `coverage_score` reports knowledge ingestion +coverage (does mathlib have a home for the concepts mentioned in +ingested papers?). To track *project-level* progress — "have we +proven the theorems we promised?" — anchor on a `goals.yaml` listing +**the actual Lean declarations** that constitute each promise: + +```yaml +goals: + - id: gns-construction + description: "Cyclic representation π_ω with ω(a)=⟨Ω_ω, π_ω(a) Ω_ω⟩." + declarations: + - GNS.Representation + - GNS.Construction.isFaithful_iff_separating + - GNS.Representation.unique_up_to_unitary_equivalence + concepts: + - GNS representation # bare string + + - id: ssa-abstract-local-net + description: "TODO. Abstract SSA over a generic local net." + declarations: [] # empty → counts as 1 missing + concepts: + - name: localNet + sources: + - { slug: "92737", anchor: { definition: "localNet" } } + - name: Tomita-Takesaki modular operator + sources: + - { slug: arxiv-2507.00900, anchor: { theorem: "2.3" } } + - { slug: arxiv-2507.00900, anchor: { section: "2.1" } } +``` + +**Two parallel concerns**, kept separate so each is judged by the +right tool: + +| Field | Truth source | Influences `goal_coverage_score`? | +| --- | --- | --- | +| `declarations` | scanner over `<lean-root>/**/*.lean` | **yes** | +| `concepts` | `references/<slug>/INDEX.md` Key concepts bullets | no — pure hint for `gap-filler` planning | + +`anchor` is a single-key map; the supported kinds are `chapter`, +`section`, `subsection`, `theorem`, `definition`, `lemma`, +`proposition`, `corollary`, `equation`, `page`, `example`. The +matcher uses only `slug` for filtering — the kind/value pair is +human-readable navigation so a developer (or `gap-filler`'s plan +output) knows exactly which page to consult. + +Pass `--goals goals.yaml --lean-root QuantumSystem` (or whatever your +Lean tree is) to step 1 to get the per-goal block. Without +`--lean-root`, declarations are tagged `unverified` rather than +guessed — `goal_coverage_score` then reads as the absence of evidence. + +## 1. Detect gaps + +```bash +python3 .claude/skills/gap-filler/scripts/detect_gaps.py \ + references/ --target-slug arxiv-2202.03357 --output references/gaps.json +``` + +Expected shape of `gaps.json` (truncated): + +```json +{ + "target_slug": "arxiv-2202.03357", + "counts": { + "formalized": 1, + "resolved": 2, + "partial": 0, + "suspect": 1, + "gaps": 10, + "ambiguous": 0, + "other_knowledge": 0 + }, + "issues": {"open": 1, "directory": "references/issues"}, + "coverage_score": 0.214, + "formalized": [ + {"concept": "Umegaki relative entropy", "sources": [...], + "formalized_annotation": "→ formalized: QuantumSystem.RelativeEntropy.umegaki"} + ], + "resolved": [ + {"concept": "C*-algebra", + "mathlib_annotation": "→ mathlib: Mathlib.Analysis.CStarAlgebra.Classes", + "sources": [{"slug": "arxiv-2202.03357", "annotation": "..."}]} + ], + "suspect": [ + {"concept": "Modular automorphism group", + "mathlib_annotation": "→ mathlib: Mathlib.Foo.Bar [UNVERIFIED] (...)", + "sources": [...]} + ], + "gaps": [ + {"concept": "Araki relative entropy", "sources": [...]}, + {"concept": "Kosaki variational formula", "sources": [...]}, + {"concept": "Jones index", "sources": [...]} + ] +} +``` + +With `--goals goals.yaml --lean-root QuantumSystem` the report also +carries: + +```json +{ + "lean_root": "/abs/path/QuantumSystem", + "lean_declarations_count": 714, + "goals_summary": { + "total": 8, + "satisfied": 7, + "partially_satisfied": 0, + "missing": 1, + "unverified": 0, + "declarations_total": 20, + "declarations_verified": 19, + "goal_coverage_score": 0.95, + "formula": "verified_declarations / total_declarations" + }, + "goals": [ + {"id": "gns-construction", + "goal_status": "satisfied", + "declarations": [ + {"name": "GNS.Representation", "status": "verified"}, + {"name": "GNS.Construction.isFaithful_iff_separating", "status": "verified"} + ], + "missing_declarations": [], + "concepts": [{"name": "GNS representation", + "status": "gap", + "matched_sources": [{"slug": "92737", "annotation": "..."}]}]}, + {"id": "ssa-abstract-local-net", + "goal_status": "missing", + "declarations": [], + "missing_declarations": [], + "missing_concepts": ["Tomita-Takesaki modular operator"]} + ] +} +``` + +The TODO goal contributes 1 to `declarations_total` (so empty +`declarations: []` does not silently inflate the score) but 0 to +`declarations_verified`. + +## 2. Rank the bibliography + +```bash +python3 .claude/skills/gap-filler/scripts/rank_bibliography.py \ + references/arxiv-2202.03357/ \ + --output references/arxiv-2202.03357/bibliography-ranked.json +``` + +Expected top of `uninvested_top` (abridged; each entry now also carries +a `suggested_search_queries` list). **Query ordering depends on the +entry's publication year**: + +- ``year >= 1995`` (modern): `university-pdf:<domain>` rotation is listed + first (faculty pages often host the paper or author's lecture notes), + then `lecture-notes`, then `nlab`/`wikipedia`. +- ``year < 1995`` (legacy): `lecture-notes` leads, followed by the + open-access archives `numdam` and `projecteuclid` and a bare + `filetype:pdf` pass. University-PDF rotation is **demoted to the + tail** — iteration-2 showed university domains almost never host + 1980s-era operator-algebra journal papers, so burning WebSearch + budget on them first is wasteful. + +The cutoff is empirical (1995 ≈ onset of institutional preprint +hosting) and editable in +`gap-filler/scripts/rank_bibliography.py::PRE_INSTITUTIONAL_HOSTING_YEAR`. +When `year` is absent from the bibliography entry, the modern ordering +is used as a safe default. + +```json +[ + { + "key": "Jon83", "title": "Index for subfactors", + "authors": ["Vaughan Jones"], "year": 1983, + "arxiv": null, "doi": null, "ingested": false, + "citations_raw": 13, "citation_score": 19.0, + "matched_token": "Jon83", + "suggested_search_queries": [ + {"strategy": "lecture-notes", + "query": "Index subfactors Jones \"lecture notes\" filetype:pdf"}, + {"strategy": "numdam", + "query": "Index subfactors Jones site:numdam.org"}, + {"strategy": "project-euclid", + "query": "Index subfactors Jones site:projecteuclid.org"}, + {"strategy": "open-access-pdf", + "query": "Index subfactors Jones filetype:pdf"}, + {"strategy": "nlab", "query": "Index subfactors site:ncatlab.org"}, + {"strategy": "wikipedia", "query": "Index subfactors wikipedia"}, + {"strategy": "university-pdf:caltech.edu", + "query": "Index subfactors Jones pdf site:caltech.edu"} + ] + } +] +``` + +## 3. Synthesise a plan + +Cross-reference gaps with the ranked bibliography. **When a top entry has +no arxiv/DOI (the common case for operator algebra), try its +`suggested_search_queries` with WebSearch before falling back to +Wikipedia**. For legacy entries this means lecture notes / open-access +archives first; for modern entries it means faculty-hosted PDFs first. +Both routes usually give a cleaner treatment than encyclopedia pages: + +| Gap | Best source (preferred) | Mechanism | +|---|---|---| +| `Jones index` (Jon83) | lecture-notes PDF or open-access archive (try `lecture-notes` → `numdam` → `project-euclid` via the emitted queries) | `pdf-to-knowledge` once a PDF URL is found | +| `Kosaki variational formula` (Kos86a) | lecture-notes / open-access PDF first, nLab as fallback | `pdf-to-knowledge` or `web-to-knowledge` depending on what turns up | +| `Modular operator` / `Tomita-Takesaki` (Tak03) | Wikipedia is fine here — it is a well-maintained article | `web-to-knowledge` | + +Fall back to Wikipedia / nLab only when the PDF / archive search finds +nothing relevant. The trade-off: WebSearch costs a few tool calls per +concept, but the resulting PDFs tend to carry definitions, proofs, and +worked examples in one place — far more useful than stitching together +a Wikipedia stub plus scattered nLab entries. + +A typical plan covers the 3 gaps with the highest intersection of +"blocks many other concepts" and "has a discoverable URL" — the three +rows above. + +## 4. Execute (with user approval) + +For the first two entries, call `web-to-knowledge`: + +```bash +uv run .claude/skills/web-to-knowledge/scripts/fetch.py \ + "https://en.wikipedia.org/wiki/Tomita%E2%80%93Takesaki_theory" +uv run .claude/skills/web-to-knowledge/scripts/fetch.py \ + "https://ncatlab.org/nlab/show/relative+entropy" +``` + +Then **always** refresh the concept index: + +```bash +python3 .claude/skills/pdf-to-knowledge/scripts/update_concepts.py references/ +``` + +## 5. Re-measure + +Run step 1 again. Expected delta: + +- `resolved` grows by any concepts that now carry a `→ mathlib:` + annotation on the freshly ingested INDEX.md (Wikipedia Tomita-Takesaki + typically resolves `VonNeumannAlgebra.commutant`; nLab relative + entropy resolves `InformationTheory.klDiv`, `MeasureTheory.rnDeriv`). +- `gaps` shrinks by the resolved count. +- `other_knowledge` grows — bullets from the new slugs that the target + paper does not mention directly but which supplement the topic. + +## Side channel — issue tracker (`references/issues/`) + +When `verify_mathlib_refs.py mark-unverified` flags a bullet, it +auto-creates a YAML under `references/issues/` so the false positive is +not forgotten across sessions. Re-running the same loop is a no-op (the +dedup key is `kind + slug + concept + candidate`): + +```bash +# Manually open an issue (e.g. paper-notation-refactor skipped a candidate) +python3 .claude/skills/gap-filler/scripts/issues.py add references \ + --kind notation-skipped \ + --slug arxiv-2202.03357 \ + --concept "modular automorphism group" \ + --reason "Mathlib scope conflict on σ" + +python3 .claude/skills/gap-filler/scripts/issues.py list references +python3 .claude/skills/gap-filler/scripts/issues.py close references \ + --kind unverified-mathlib-ref --slug arxiv-2202.03357 \ + --closed-by "human review" +``` + +`detect_gaps.py` surfaces `report.issues.open`; treat that count as the +"system already knows about" backlog complementary to `gaps`. A typical +pattern across one ingestion cycle: + +``` +baseline: formalized=1 resolved=1 gap=12 issues=0 cov=0.214 +after lean_verify rejects modular operator: + formalized=1 suspect=1 gap=12 issues=1 cov=0.143 +after notation-refactor adds → formalized: for it: + formalized=2 resolved=0 gap=12 issues=0 cov=0.214 +``` + +Note that the third row's `coverage_score` returns to baseline even +though the underlying state changed — the project just discovered that +mathlib's annotation was wrong and replaced it with a local proof. The +trajectory shows up clearly in the history log. + +## Side channel — progress history (`references/gaps-history.jsonl`) + +Each `detect_gaps.py` run appends one record. Quick way to see what +moved the needle: + +```bash +jq -c '{ts: .timestamp, cov: .coverage_score, goal: .goals.goal_coverage_score, issues: .issues_open, fmlz: .counts.formalized, susp: .counts.suspect}' \ + references/gaps-history.jsonl +``` + +Sample output across a 5-step cycle: + +``` +{"ts":"2026-05-04T10:00:00Z","cov":0.5,"goal":0.667,"issues":0,"fmlz":1,"susp":0} +{"ts":"2026-05-04T10:05:00Z","cov":0.25,"goal":0.333,"issues":1,"fmlz":1,"susp":1} +{"ts":"2026-05-04T10:10:00Z","cov":0.5,"goal":0.667,"issues":0,"fmlz":2,"susp":0} +``` + +Pass `--no-history` to suppress, or `--history-log path/elsewhere.jsonl` +to redirect when the default `references/` tree is gitignored. + +## When to stop + +- `gaps` shrinks to a stable set whose entries are genuinely unformalised + in mathlib (no amount of recursive ingestion helps). +- The only remaining sources lack discoverable URLs (pre-arxiv 1970s + math journals) — promote those to the user as "needs human action". +- The ingestion budget (default 3 per invocation) has been used; ask the + user before approving another round. diff --git a/.claude/skills/gap-filler/scripts/detect_gaps.py b/.claude/skills/gap-filler/scripts/detect_gaps.py index 20888a6..26b7904 100644 --- a/.claude/skills/gap-filler/scripts/detect_gaps.py +++ b/.claude/skills/gap-filler/scripts/detect_gaps.py @@ -8,13 +8,27 @@ A concept is classified by looking at the annotation on its Key concepts bullet across every ``<slug>/INDEX.md`` under the root: +- ``→ formalized: QuantumSystem.X.y`` → **formalized** (already proven in + this repository — outranks ``resolved`` for prioritisation). - ``→ mathlib: Mathlib.X.y`` → **resolved** (mathlib already has it). - ``→ needs formalization`` → **gap** (no mathlib coverage). - No annotation → **ambiguous** (treat as potential gap). Concepts with the same normalised name coming from multiple sources are -merged; the aggregate classification is "resolved" if any source says so, -otherwise "gap" unless every annotation is "ambiguous". +merged; the aggregate classification picks the strongest tier present — +``formalized`` beats ``resolved`` beats ``partial`` beats ``gap`` beats +``ambiguous``. ``suspect`` (a mathlib annotation that ``verify_mathlib_refs.py`` +flagged as ``[UNVERIFIED]``) is reported separately so a previously +trusted answer that turned out wrong is more visible than a fresh gap. + +Optionally, ``--goals path/to/goals.yaml`` constrains the coverage score +to a fixed list of target concepts (the project's actual formalization +goals). Without ``--goals`` the universe is "every concept ingested under +references/" — useful for raw progress, but the denominator drifts as +new papers are added. With ``--goals`` the score answers the operative +question: "of the concepts I committed to formalize, what fraction is +done?". Goal concepts not yet present in any INDEX.md are classified as +``unknown`` and counted as gaps for the coverage formula. Usage: python3 detect_gaps.py <references-root> [--target-slug SLUG] @@ -33,6 +47,7 @@ from __future__ import annotations import argparse +import datetime as _dt import json import re import sys @@ -45,8 +60,14 @@ BULLET = re.compile(r"^\s*-\s+(.*)$") LEADING_CODE = re.compile(r"^`([^`]+)`(.*)$") MATHLIB_ANNOT = re.compile(r"→\s*mathlib\s*:", re.IGNORECASE) +FORMALIZED_ANNOT = re.compile(r"→\s*formalized\s*:", re.IGNORECASE) NEEDS_FORMAL_ANNOT = re.compile(r"→\s*needs\s*formalization", re.IGNORECASE) UNVERIFIED_MARKER = re.compile(r"\[UNVERIFIED\]", re.IGNORECASE) +LEAN_DECL_NAME = re.compile(r"^[A-Za-z_][\w']*(?:\.[A-Za-z_][\w']*)*$") + + +class GoalsValidationError(ValueError): + """Raised when goals.yaml violates the supported contract.""" def _strip_front_annotation_markers(body: str) -> tuple[str, str]: @@ -229,7 +250,13 @@ def parse_key_concepts(md: str) -> list[dict]: display = body.split("—", 1)[0].split(":", 1)[0].split("(", 1)[0].strip()[:60] rest = body description, annotation = _strip_front_annotation_markers(rest) - if MATHLIB_ANNOT.search(annotation) and UNVERIFIED_MARKER.search(annotation): + if FORMALIZED_ANNOT.search(annotation) and UNVERIFIED_MARKER.search(annotation): + # A `→ formalized:` annotation that failed `verify_mathlib_refs.py` + # — same treatment as a suspect mathlib annotation. + status = "suspect" + elif FORMALIZED_ANNOT.search(annotation): + status = "formalized" + elif MATHLIB_ANNOT.search(annotation) and UNVERIFIED_MARKER.search(annotation): # A mathlib annotation that failed `verify_mathlib_refs.py` — do # not trust it. Downstream prioritisation should treat this as a # gap that also flags the previous search result as wrong. @@ -268,6 +295,543 @@ def _read_frontmatter_slug(md: str, fallback: str) -> str: return fallback +# --- goals.yaml (bespoke YAML-subset parser, no PyYAML dep) --- +# +# Supported shape: +# +# goals: +# - id: gns-construction +# description: "Cyclic representation π_ω …" +# declarations: +# - GNS.Representation +# - GNS.Construction.isFaithful_iff_separating +# concepts: +# - "GNS representation" # bare string +# - name: "Tomita-Takesaki modular operator" # structured +# sources: +# - { slug: arxiv-2507.00900, anchor: { theorem: "2.3" } } +# - { slug: 92737, anchor: { definition: "modular operator" } } +# +# What the parser handles: +# - Top-level ``goals:`` block list +# - Each goal is a block mapping with arbitrary keys +# - Block lists under any key (declarations, concepts, sources, …) +# - List items can be bare scalars, inline flow mappings ``{ ... }``, +# or block mappings introduced by ``- key: value`` +# - Single-line inline flow mappings nest (``{ slug: a, anchor: { ... } }``) +# +# Indentation is taken at face value; 2-space steps are conventional but +# not enforced. The parser handles YAML-style inline comments and simple +# block scalars (`>` / `>-` / `|` / `|-`) because the checked-in +# goals.yaml uses them. It does not handle YAML anchors/tags/merge keys. + + +_INLINE_KEY_RE = re.compile(r"\s*([A-Za-z_][\w-]*)\s*:\s*") + + +def _strip_quote(value: str) -> str: + value = value.strip() + if (value.startswith('"') and value.endswith('"')) or ( + value.startswith("'") and value.endswith("'") + ): + return value[1:-1] + return value + + +def _coerce_scalar(text: str): + """Best-effort YAML scalar coercion (string / int / float / bool / null).""" + text = text.strip() + if not text: + return None + if (text.startswith('"') and text.endswith('"')) or ( + text.startswith("'") and text.endswith("'") + ): + return text[1:-1] + if text in ("null", "~"): + return None + if text == "true": + return True + if text == "false": + return False + try: + return int(text) + except ValueError: + pass + try: + return float(text) + except ValueError: + pass + return text + + +def _strip_inline_comment(text: str) -> str: + """Drop YAML-style inline comments while preserving quoted/flow content.""" + out: list[str] = [] + in_single = False + in_double = False + brace_depth = 0 + bracket_depth = 0 + for idx, ch in enumerate(text): + if ch == "'" and not in_double: + in_single = not in_single + out.append(ch) + continue + if ch == '"' and not in_single: + in_double = not in_double + out.append(ch) + continue + if not in_single and not in_double: + if ch == "{": + brace_depth += 1 + elif ch == "}" and brace_depth > 0: + brace_depth -= 1 + elif ch == "[": + bracket_depth += 1 + elif ch == "]" and bracket_depth > 0: + bracket_depth -= 1 + elif ( + ch == "#" + and brace_depth == 0 + and bracket_depth == 0 + and (idx == 0 or text[idx - 1].isspace()) + ): + break + out.append(ch) + return "".join(out).rstrip() + + +def _is_block_scalar_marker(text: str) -> bool: + text = text.strip() + return bool(text) and text[0] in ">|" and set(text[1:]) <= {"-", "+"} + + +def _fold_block_scalar(lines: list[str], marker: str) -> str: + stripped = [line.strip() for line in lines] + if not stripped: + return "" + if marker.startswith("|"): + return "\n".join(stripped) + return " ".join(part for part in stripped if part) + + +def _read_inline_value(s: str, pos: int): + """Read a single value (quoted string, nested flow mapping, flow list, + or bare scalar up to the next comma) from ``s`` starting at ``pos``. + Returns ``(value, new_pos)``.""" + n = len(s) + while pos < n and s[pos] == " ": + pos += 1 + if pos >= n: + return None, pos + if s[pos] == "{": + depth = 1 + start = pos + pos += 1 + while pos < n and depth > 0: + if s[pos] == "{": + depth += 1 + elif s[pos] == "}": + depth -= 1 + pos += 1 + return _parse_inline_mapping(s[start:pos]), pos + if s[pos] == "[": + depth = 1 + start = pos + pos += 1 + while pos < n and depth > 0: + if s[pos] == "[": + depth += 1 + elif s[pos] == "]": + depth -= 1 + pos += 1 + return _parse_inline_list(s[start:pos]), pos + if s[pos] in '"\'': + quote = s[pos] + pos += 1 + start = pos + while pos < n and s[pos] != quote: + pos += 1 + value = s[start:pos] + if pos < n: + pos += 1 + return value, pos + start = pos + while pos < n and s[pos] != ",": + pos += 1 + return _coerce_scalar(s[start:pos]), pos + + +def _parse_inline_mapping(text: str) -> dict: + """Parse a YAML flow mapping like ``{ a: b, c: { d: e } }``.""" + text = text.strip() + if not (text.startswith("{") and text.endswith("}")): + raise ValueError(f"expected inline mapping: {text!r}") + inner = text[1:-1] + result: dict = {} + pos = 0 + n = len(inner) + while pos < n: + while pos < n and inner[pos] in " ,": + pos += 1 + if pos >= n: + break + m = _INLINE_KEY_RE.match(inner, pos) + if not m: + raise ValueError(f"missing key at pos {pos} in {text!r}") + key = m.group(1) + pos = m.end() + value, pos = _read_inline_value(inner, pos) + result[key] = value + return result + + +def _parse_inline_list(text: str) -> list: + """Parse a YAML flow list like ``[a, b, "c", {d: e}]``. Empty ``[]`` → ``[]``.""" + text = text.strip() + if not (text.startswith("[") and text.endswith("]")): + raise ValueError(f"expected inline list: {text!r}") + inner = text[1:-1] + result: list = [] + pos = 0 + n = len(inner) + while pos < n: + while pos < n and inner[pos] in " ,": + pos += 1 + if pos >= n: + break + value, pos = _read_inline_value(inner, pos) + result.append(value) + return result + + +class _YamlMiniParser: + """Indentation-aware parser for the goals.yaml subset described above.""" + + _KEY_RE = re.compile(r"^([A-Za-z_][\w-]*)\s*:\s*(.*)$") + + def __init__(self, text: str) -> None: + self.tokens: list[tuple[int, str]] = [] + for raw in text.splitlines(): + cleaned = _strip_inline_comment(raw) + stripped_lhs = cleaned.lstrip() + if not stripped_lhs or stripped_lhs.startswith("#"): + continue + indent = len(cleaned) - len(stripped_lhs) + self.tokens.append((indent, stripped_lhs.rstrip())) + self.pos = 0 + + def _peek(self) -> tuple[int, str] | None: + return self.tokens[self.pos] if self.pos < len(self.tokens) else None + + def _parse_block_scalar(self, base_indent: int, marker: str) -> str: + lines: list[str] = [] + while self._peek() is not None: + ti, tc = self._peek() + if ti <= base_indent: + break + self.pos += 1 + lines.append(tc) + return _fold_block_scalar(lines, marker) + + def parse_block_mapping(self, indent: int) -> dict: + result: dict = {} + while self._peek() is not None: + ti, tc = self._peek() + if ti < indent or tc.startswith("- "): + break + if ti > indent: + # Over-indented stray line — should have been consumed by recursion. + self.pos += 1 + continue + m = self._KEY_RE.match(tc) + if not m: + break + self.pos += 1 + key = m.group(1) + v_text = m.group(2).strip() + if not v_text: + result[key] = self._parse_value_below(indent + 2) + elif _is_block_scalar_marker(v_text): + result[key] = self._parse_block_scalar(indent, v_text) + elif v_text.startswith("{"): + result[key] = _parse_inline_mapping(v_text) + elif v_text.startswith("["): + result[key] = _parse_inline_list(v_text) + else: + result[key] = _coerce_scalar(v_text) + return result + + def parse_block_list(self, indent: int) -> list: + items: list = [] + while self._peek() is not None: + ti, tc = self._peek() + if ti != indent or not tc.startswith("- "): + break + self.pos += 1 + rest = tc[2:].lstrip() + if rest.startswith("{"): + items.append(_parse_inline_mapping(rest)) + continue + m = self._KEY_RE.match(rest) + if m: + first_key = m.group(1) + v_text = m.group(2).strip() + if not v_text: + first_value = self._parse_value_below(indent + 4) + elif _is_block_scalar_marker(v_text): + first_value = self._parse_block_scalar(indent + 2, v_text) + elif v_text.startswith("{"): + first_value = _parse_inline_mapping(v_text) + else: + first_value = _coerce_scalar(v_text) + tail = self.parse_block_mapping(indent + 2) + merged: dict = {first_key: first_value} + merged.update(tail) + items.append(merged) + continue + items.append(_coerce_scalar(rest)) + return items + + def _parse_value_below(self, expected_indent: int): + peek = self._peek() + if peek is None or peek[0] < expected_indent: + return None + ti, tc = peek + if tc.startswith("- "): + return self.parse_block_list(ti) + if self._KEY_RE.match(tc): + return self.parse_block_mapping(ti) + # Defensive: skip and return None + return None + + +def parse_goals_yaml(text: str) -> list[dict]: + """Parse a constrained goals.yaml subset. Returns a list of goal dicts.""" + parser = _YamlMiniParser(text) + while parser._peek() is not None: + ti, tc = parser._peek() + if ti == 0 and re.match(r"^goals\s*:\s*$", tc): + parser.pos += 1 + break + parser.pos += 1 + else: + return [] + peek = parser._peek() + if peek is None or not peek[1].startswith("- "): + return [] + return parser.parse_block_list(peek[0]) + + +def load_goals(path: Path) -> list[dict]: + text = path.read_text(encoding="utf-8", errors="replace") + return validate_goals(parse_goals_yaml(text), source_name=str(path)) + + +def _raise_goals_validation(source_name: str, message: str) -> None: + raise GoalsValidationError(f"{source_name}: {message}") + + +def _validate_nonempty_string(value, path: str, source_name: str) -> str: + if not isinstance(value, str): + _raise_goals_validation(source_name, f"{path} must be a non-empty string") + text = value.strip() + if not text: + _raise_goals_validation(source_name, f"{path} must be a non-empty string") + return text + + +def _validate_slug_like(value, path: str, source_name: str) -> str: + if value is None or isinstance(value, bool): + _raise_goals_validation(source_name, f"{path} must be a non-empty slug") + text = str(value).strip() + if not text: + _raise_goals_validation(source_name, f"{path} must be a non-empty slug") + return text + + +def _validate_anchor(anchor, path: str, source_name: str): + if not isinstance(anchor, dict) or len(anchor) != 1: + _raise_goals_validation( + source_name, + f"{path} must be a single-key mapping like {{ section: '2.1' }}", + ) + key, value = next(iter(anchor.items())) + key_text = _validate_nonempty_string(key, f"{path} key", source_name) + if isinstance(value, (dict, list)): + _raise_goals_validation(source_name, f"{path}.{key_text} must be a scalar") + return {key_text: value} + + +def _validate_source_entry(source_entry, path: str, source_name: str) -> dict: + if not isinstance(source_entry, dict): + _raise_goals_validation(source_name, f"{path} must be a mapping") + if "slug" not in source_entry: + _raise_goals_validation(source_name, f"{path}.slug is required") + normalized = dict(source_entry) + normalized["slug"] = _validate_slug_like(source_entry.get("slug"), f"{path}.slug", source_name) + if "anchor" in source_entry and source_entry.get("anchor") is not None: + normalized["anchor"] = _validate_anchor(source_entry.get("anchor"), f"{path}.anchor", source_name) + return normalized + + +def _validate_concept_entry(concept_entry, path: str, source_name: str): + if isinstance(concept_entry, str): + return _validate_nonempty_string(concept_entry, path, source_name) + if not isinstance(concept_entry, dict): + _raise_goals_validation(source_name, f"{path} must be a string or mapping") + normalized = dict(concept_entry) + normalized["name"] = _validate_nonempty_string(concept_entry.get("name"), f"{path}.name", source_name) + sources = concept_entry.get("sources") + if sources is None: + return normalized + if not isinstance(sources, list): + _raise_goals_validation(source_name, f"{path}.sources must be a list") + normalized["sources"] = [ + _validate_source_entry(source, f"{path}.sources[{idx}]", source_name) + for idx, source in enumerate(sources) + ] + return normalized + + +def _validate_declarations(declarations, path: str, source_name: str) -> list[str]: + if not isinstance(declarations, list): + _raise_goals_validation(source_name, f"{path} must be a list") + normalized: list[str] = [] + for idx, decl in enumerate(declarations): + text = _validate_nonempty_string(decl, f"{path}[{idx}]", source_name) + if not LEAN_DECL_NAME.match(text): + _raise_goals_validation( + source_name, + f"{path}[{idx}] must be a dotted Lean declaration name", + ) + normalized.append(text) + return normalized + + +def validate_goals(goals, *, source_name: str = "goals.yaml") -> list[dict]: + """Validate and normalize the parsed goals.yaml structure.""" + if not isinstance(goals, list) or not goals: + _raise_goals_validation( + source_name, + "expected a non-empty top-level `goals:` list", + ) + + normalized_goals: list[dict] = [] + seen_ids: set[str] = set() + for idx, goal in enumerate(goals): + path = f"goals[{idx}]" + if not isinstance(goal, dict): + _raise_goals_validation(source_name, f"{path} must be a mapping") + goal_id = _validate_nonempty_string(goal.get("id"), f"{path}.id", source_name) + if goal_id in seen_ids: + _raise_goals_validation(source_name, f"duplicate goal id: {goal_id}") + seen_ids.add(goal_id) + + normalized = dict(goal) + normalized["id"] = goal_id + normalized["description"] = _validate_nonempty_string( + goal.get("description"), f"{path}.description", source_name + ) + normalized["declarations"] = _validate_declarations( + goal.get("declarations"), f"{path}.declarations", source_name + ) + + concepts = goal.get("concepts") + if concepts is None: + normalized["concepts"] = [] + else: + if not isinstance(concepts, list): + _raise_goals_validation(source_name, f"{path}.concepts must be a list") + normalized["concepts"] = [ + _validate_concept_entry( + concept, + f"{path}.concepts[{concept_idx}]", + source_name, + ) + for concept_idx, concept in enumerate(concepts) + ] + normalized_goals.append(normalized) + + return normalized_goals + + +# --- Lean source scanner (used by `--lean-root`) --------------------------- + +# Decl-keyword line. The optional prefix block matches the modifiers and +# attribute brackets that may legally precede the keyword. The trailing +# group captures the declaration's short name. +_LEAN_DECL_RE = re.compile( + r""" + ^\s* + (?:(?:noncomputable|private|protected|partial|nonrec|unsafe|@\[[^\]]*\])\s+)* + (theorem|lemma|def|structure|class|instance|inductive|abbrev|axiom|opaque) + \s+ + (?:@\[[^\]]*\]\s*)* + ([A-Za-z_][\w']*) + """, + re.VERBOSE, +) +_LEAN_NAMESPACE_OPEN_RE = re.compile(r"^\s*namespace\s+([A-Za-z_][\w'.]*)\s*$") +_LEAN_SECTION_OPEN_RE = re.compile(r"^\s*section(?:\s+([A-Za-z_][\w']*))?\s*$") +_LEAN_END_RE = re.compile(r"^\s*end(?:\s+([A-Za-z_][\w'.]*))?\s*$") + + +def scan_lean_declarations(lean_root: Path) -> set[str]: + """Walk ``lean_root/**/*.lean`` and collect fully-qualified declaration + names by tracking each file's ``namespace`` / ``end`` stack. + + Sections are tracked but do not contribute to the qualified prefix + (Lean's behaviour). Anonymous declarations (``instance : ... := …``, + ``example``) are skipped because they have no name to collect. + """ + decls: set[str] = set() + for path in sorted(lean_root.rglob("*.lean")): + stack: list[tuple[str, str]] = [] # (kind, name) + in_block_comment = False + try: + text = path.read_text(encoding="utf-8", errors="replace") + except OSError: + continue + for line in text.splitlines(): + # Naive block comment handling — `/-` ... `-/` on different lines. + if in_block_comment: + idx = line.find("-/") + if idx == -1: + continue + line = line[idx + 2 :] + in_block_comment = False + while "/-" in line: + start = line.find("/-") + end = line.find("-/", start + 2) + if end == -1: + line = line[:start] + in_block_comment = True + break + line = line[:start] + line[end + 2 :] + if "--" in line: + line = line.split("--", 1)[0] + if not line.strip(): + continue + m_ns = _LEAN_NAMESPACE_OPEN_RE.match(line) + if m_ns: + stack.append(("namespace", m_ns.group(1))) + continue + m_sec = _LEAN_SECTION_OPEN_RE.match(line) + if m_sec: + stack.append(("section", m_sec.group(1) or "")) + continue + m_end = _LEAN_END_RE.match(line) + if m_end and stack: + stack.pop() + continue + m_d = _LEAN_DECL_RE.match(line) + if m_d: + name = m_d.group(2) + prefix = ".".join(item[1] for item in stack if item[0] == "namespace") + decls.add(f"{prefix}.{name}" if prefix else name) + return decls + + def collect_entries(references_root: Path) -> dict[str, list[dict]]: """Return ``{slug: [bullet_entry, ...]}`` for every ``<slug>/INDEX.md``.""" result: dict[str, list[dict]] = {} @@ -293,6 +857,7 @@ def classify_across_slugs( for entry in bullets: per_concept[entry["name"]].append((slug, entry)) + formalized: list[dict] = [] resolved: list[dict] = [] partial: list[dict] = [] suspect: list[dict] = [] @@ -304,33 +869,46 @@ def classify_across_slugs( statuses = {status for _, e in occurrences for status in (e["status"],)} display = occurrences[0][1]["display"] sources = [] - best_annotation = "" + best_mathlib = "" + best_formalized = "" other_slugs: list[str] = [] for slug, e in occurrences: sources.append({"slug": slug, "annotation": e["annotation"]}) - if "mathlib:" in e["annotation"] and not best_annotation: - best_annotation = e["annotation"] + ann = e["annotation"] + if "formalized:" in ann.lower() and not best_formalized: + best_formalized = ann + if "mathlib:" in ann and not best_mathlib: + best_mathlib = ann if slug != target_slug: other_slugs.append(slug) if target_slug is not None: from_target = any(slug == target_slug for slug, _ in occurrences) if not from_target: + other_status = _strongest_status(statuses) other_knowledge.append( { "concept": display, "sources": sources, - "status": "resolved" if "resolved" in statuses else ("gap" if "gap" in statuses else "ambiguous"), - "mathlib_annotation": best_annotation, + "status": other_status, + "mathlib_annotation": best_mathlib, + "formalized_annotation": best_formalized, } ) continue record = { "concept": display, "sources": sources, - "mathlib_annotation": best_annotation, + "mathlib_annotation": best_mathlib, + "formalized_annotation": best_formalized, "supplementary_slugs": other_slugs, } - if "suspect" in statuses and "resolved" not in statuses: + # Tier order: formalized > resolved > partial > suspect > gap > ambiguous. + # ``formalized`` always wins because a local Lean proof is the + # strongest evidence; a ``suspect`` mathlib annotation does not + # demote it. + if "formalized" in statuses: + formalized.append(record) + elif "suspect" in statuses and "resolved" not in statuses: # verify_mathlib_refs.py flagged this annotation as wrong and # no other slug provides a clean mathlib mapping. suspect.append(record) @@ -346,15 +924,24 @@ def classify_across_slugs( else: ambiguous.append(record) - # coverage_score: (resolved*1.0 + partial*0.5) / target_total. + # coverage_score weights: + # formalized = 1.0 (locally proven — strongest evidence) + # resolved = 1.0 (mathlib has it; trusted after verify_mathlib_refs) + # partial = 0.5 (target says gap, but a sibling slug documents it) # target_total excludes other_knowledge (non-target slug concepts), # because gap-filler's goal is the target's own knowledge closure. - target_total = len(resolved) + len(partial) + len(suspect) + len(gaps) + len(ambiguous) + target_total = ( + len(formalized) + len(resolved) + len(partial) + + len(suspect) + len(gaps) + len(ambiguous) + ) coverage = 0.0 if target_total: - coverage = (len(resolved) * 1.0 + len(partial) * 0.5) / target_total + coverage = ( + len(formalized) * 1.0 + len(resolved) * 1.0 + len(partial) * 0.5 + ) / target_total return { "target_slug": target_slug, + "formalized": formalized, "resolved": resolved, "partial": partial, "suspect": suspect, @@ -362,6 +949,7 @@ def classify_across_slugs( "ambiguous": ambiguous, "other_knowledge": other_knowledge, "counts": { + "formalized": len(formalized), "resolved": len(resolved), "partial": len(partial), "suspect": len(suspect), @@ -372,9 +960,220 @@ def classify_across_slugs( "coverage_score": round(coverage, 3), "coverage_breakdown": { "target_total": target_total, + "formalized_weight": 1.0, "resolved_weight": 1.0, "partial_weight": 0.5, - "formula": "(resolved*1.0 + partial*0.5) / (resolved + partial + suspect + gaps + ambiguous)", + "formula": ( + "(formalized*1.0 + resolved*1.0 + partial*0.5) / " + "(formalized + resolved + partial + suspect + gaps + ambiguous)" + ), + }, + } + + +def _all_concept_occurrences( + all_entries: dict[str, list[dict]], +) -> dict[str, list[dict]]: + """Return ``{normalised_name: [{slug, status, annotation, display}, ...]}``. + + Unlike a "best status per concept" view, this preserves every per-slug + occurrence so the goal evaluator can filter by ``sources[*].slug`` + when a concept has been pinned to specific references. + """ + out: dict[str, list[dict]] = defaultdict(list) + for slug, bullets in all_entries.items(): + for entry in bullets: + out[entry["name"]].append( + { + "slug": slug, + "status": entry["status"], + "annotation": entry["annotation"], + "display": entry["display"], + } + ) + return out + + +def _best_status(occurrences: list[dict]) -> str: + """Pick the strongest tier from a list of per-slug occurrence records.""" + statuses = {o["status"] for o in occurrences} + if not statuses: + return "unknown" + return _strongest_status(statuses) + + +def _strongest_status(statuses: set[str]) -> str: + """Pick the strongest concept tier from a set of statuses.""" + if "formalized" in statuses: + return "formalized" + if "resolved" in statuses: + return "resolved" + if "suspect" in statuses: + return "suspect" + if "gap" in statuses: + return "gap" + return "ambiguous" + + +def _evaluate_concept_entry( + concept_entry, + occurrences_map: dict[str, list[dict]], +) -> dict: + """Resolve one ``concepts:`` list element against the references tree. + + ``concept_entry`` is either a bare string (any slug counts) or a + ``{name, sources}`` mapping where each source pins the concept to a + specific ``slug`` (and optionally a free-form ``anchor`` for human + navigation). When ``sources`` is given, only matching slugs are + consulted; if none of the wanted slugs document the concept, status + is ``unknown``. + """ + if isinstance(concept_entry, str): + name = concept_entry + sources_filter: list = [] + elif isinstance(concept_entry, dict): + name = str(concept_entry.get("name") or "") + sources_filter = concept_entry.get("sources") or [] + else: + name = str(concept_entry) + sources_filter = [] + + normalised = _normalise_concept(name) + occurrences = occurrences_map.get(normalised, []) + + if sources_filter: + wanted = { + str(s.get("slug")) + for s in sources_filter + if isinstance(s, dict) and s.get("slug") is not None + } + filtered = [o for o in occurrences if str(o["slug"]) in wanted] + else: + filtered = occurrences + + return { + "name": name, + "normalized": normalised, + "status": _best_status(filtered), + "sources_hint": sources_filter, + "matched_sources": [ + {"slug": o["slug"], "annotation": o["annotation"]} for o in filtered + ], + } + + +def _verify_declarations(decls: list[str], lean_decls: set[str] | None) -> list[dict]: + """Tag each declaration name with ``verified`` / ``missing`` / ``unverified``. + + ``unverified`` means the caller did not pass ``--lean-root``, so the + Lean source could not be scanned; this is a soft state, distinct + from "we looked and could not find it". + """ + if lean_decls is None: + return [{"name": d, "status": "unverified"} for d in decls] + return [ + {"name": d, "status": "verified" if d in lean_decls else "missing"} + for d in decls + ] + + +def evaluate_goals( + all_entries: dict[str, list[dict]], + goals: list[dict], + lean_decls: set[str] | None = None, +) -> dict: + """Score each goal against the project's Lean source and references tree. + + A goal is satisfied when every name in its ``declarations`` list is + present in the scanned Lean tree. ``concepts`` is *informational* — + it indicates which prerequisite knowledge the goal depends on, so + ``gap-filler`` can suggest what to ingest next, but it does not + enter the satisfaction judgement. When ``lean_decls`` is ``None`` + (no ``--lean-root`` passed) every goal is reported as ``unverified`` + rather than guessed. + + Coverage formula: ``verified_declarations / total_declarations`` over + every goal. Goals declared with an empty ``declarations: []`` (TODOs) + contribute one missing slot to the denominator so they show up as + incomplete. + """ + occurrences_map = _all_concept_occurrences(all_entries) + goal_records: list[dict] = [] + + total_decls = 0 + verified_decls = 0 + + sat = part = miss = unverified_count = 0 + + for goal in goals: + decls = goal.get("declarations") or [] + decl_results = _verify_declarations(decls, lean_decls) + verified_in_goal = sum(1 for r in decl_results if r["status"] == "verified") + missing_in_goal = sum(1 for r in decl_results if r["status"] == "missing") + + # Coverage accounting. Empty-declaration goals count as one missing + # slot so untouched TODOs do not silently inflate the score. + if not decls: + total_decls += 1 + else: + total_decls += len(decls) + verified_decls += verified_in_goal + + # Goal-level status. + if not decls: + goal_status = "missing" + miss += 1 + elif lean_decls is None: + goal_status = "unverified" + unverified_count += 1 + elif missing_in_goal == 0: + goal_status = "satisfied" + sat += 1 + elif verified_in_goal == 0: + goal_status = "missing" + miss += 1 + else: + goal_status = "partially_satisfied" + part += 1 + + # Concept evaluation — informational only, used by gap-filler hints. + concept_results = [ + _evaluate_concept_entry(c, occurrences_map) + for c in (goal.get("concepts") or []) + ] + + goal_records.append( + { + "id": goal.get("id"), + "description": goal.get("description"), + "declarations": decl_results, + "concepts": concept_results, + "missing_declarations": [ + r["name"] for r in decl_results if r["status"] == "missing" + ], + "missing_concepts": [ + c["name"] + for c in concept_results + if c["status"] in ("unknown", "ambiguous", "gap", "suspect") + ], + "goal_status": goal_status, + } + ) + + coverage = (verified_decls / total_decls) if total_decls else 0.0 + + return { + "goals": goal_records, + "goals_summary": { + "total": len(goals), + "satisfied": sat, + "partially_satisfied": part, + "missing": miss, + "unverified": unverified_count, + "declarations_total": total_decls, + "declarations_verified": verified_decls, + "goal_coverage_score": round(coverage, 3), + "formula": "verified_declarations / total_declarations", }, } @@ -383,7 +1182,42 @@ def main() -> int: parser = argparse.ArgumentParser(description=__doc__) parser.add_argument("references_root", help="Directory that contains per-slug subdirs") parser.add_argument("--target-slug", default=None, help="Slug whose gaps we care about") + parser.add_argument( + "--goals", + default=None, + help=( + "Path to a goals.yaml that lists the formalization targets. " + "When given, the report adds a per-goal status block. Goal " + "satisfaction is decided by `declarations` (verified against " + "the Lean tree at --lean-root); `concepts` is informational." + ), + ) + parser.add_argument( + "--lean-root", + default=None, + help=( + "Path to the Lean source tree (e.g. ./QuantumSystem). Each " + "goal's `declarations` is checked against the set of " + "fully-qualified theorem/def/structure/class/instance names " + "found by walking <lean-root>/**/*.lean. Without this flag, " + "declarations are reported as `unverified`." + ), + ) parser.add_argument("--output", default=None, help="Write JSON here; default: stdout") + parser.add_argument( + "--history-log", + default=None, + help=( + "Append a one-line JSON record per run to this path. Default: " + "<references-root>/gaps-history.jsonl (skipped only when " + "--no-history is also passed)." + ), + ) + parser.add_argument( + "--no-history", + action="store_true", + help="Suppress the append-only history log entirely.", + ) args = parser.parse_args() root = Path(args.references_root).expanduser().resolve() @@ -394,10 +1228,88 @@ def main() -> int: all_entries = collect_entries(root) report = classify_across_slugs(all_entries, args.target_slug) + # Surface the live issue count so the user sees outstanding items + # (false-positive mathlib refs, skipped notation candidates, …) + # alongside the concept-tier breakdown. + issues_dir = root / "issues" + if issues_dir.is_dir(): + report["issues"] = { + "open": sum( + 1 + for entry in issues_dir.iterdir() + if entry.is_file() and entry.suffix == ".yaml" + ), + "directory": str(issues_dir), + } + else: + report["issues"] = {"open": 0, "directory": str(issues_dir)} + + lean_decls: set[str] | None = None + if args.lean_root: + lean_root = Path(args.lean_root).expanduser().resolve() + if not lean_root.is_dir(): + print(f"[error] not a directory: {lean_root}", file=sys.stderr) + return 2 + lean_decls = scan_lean_declarations(lean_root) + report["lean_root"] = str(lean_root) + report["lean_declarations_count"] = len(lean_decls) + + if args.goals: + goals_path = Path(args.goals).expanduser().resolve() + if not goals_path.is_file(): + print(f"[error] goals file not found: {goals_path}", file=sys.stderr) + return 2 + try: + goals = load_goals(goals_path) + except GoalsValidationError as exc: + print(f"[error] invalid goals file: {exc}", file=sys.stderr) + return 2 + report["goals_file"] = str(goals_path) + report.update(evaluate_goals(all_entries, goals, lean_decls)) + + if not args.no_history: + history_path = ( + Path(args.history_log).expanduser().resolve() + if args.history_log + else root / "gaps-history.jsonl" + ) + record: dict = { + "timestamp": _dt.datetime.now(_dt.timezone.utc).isoformat(timespec="seconds"), + "target_slug": args.target_slug, + "coverage_score": report["coverage_score"], + "counts": report["counts"], + "issues_open": report["issues"]["open"], + } + if args.goals: + gs = report["goals_summary"] + record["goals"] = { + "total": gs["total"], + "satisfied": gs["satisfied"], + "partially_satisfied": gs["partially_satisfied"], + "missing": gs["missing"], + "unverified": gs.get("unverified", 0), + "declarations_total": gs.get("declarations_total", 0), + "declarations_verified": gs.get("declarations_verified", 0), + "goal_coverage_score": gs["goal_coverage_score"], + } + history_path.parent.mkdir(parents=True, exist_ok=True) + with history_path.open("a", encoding="utf-8") as fh: + fh.write(json.dumps(record, ensure_ascii=False) + "\n") + report["history_log"] = str(history_path) + payload = json.dumps(report, indent=2, ensure_ascii=False) if args.output: Path(args.output).write_text(payload + "\n", encoding="utf-8") - print(f"[ok] wrote {args.output}: {report['counts']}", file=sys.stderr) + summary_msg = f"[ok] wrote {args.output}: {report['counts']}" + if report["issues"]["open"]: + summary_msg += f" | open issues: {report['issues']['open']}" + if args.goals: + gs = report["goals_summary"] + summary_msg += ( + f" | goals: {gs['satisfied']}/{gs['total']} satisfied, " + f"goal_coverage_score={gs['goal_coverage_score']}" + ) + print(summary_msg, file=sys.stderr) else: print(payload) return 0 diff --git a/goals.yaml b/goals.yaml new file mode 100644 index 0000000..36b19f2 --- /dev/null +++ b/goals.yaml @@ -0,0 +1,120 @@ +# Formalization targets for QuantumSystem. +# +# `declarations` is the **truth source**: each goal is satisfied iff every +# fully-qualified Lean name in `declarations` exists in the project's Lean +# tree. Run with: +# +# python3 .claude/skills/gap-filler/scripts/detect_gaps.py \ +# references/ --goals goals.yaml --lean-root QuantumSystem \ +# --output references/gaps.json +# +# `concepts` is **informational**: it lists the prerequisite knowledge a +# goal depends on. `gap-filler` uses these hints to plan ingestions but +# they do not affect goal satisfaction. Each concept may be a bare string +# (any references/<slug>/INDEX.md mentioning it counts) or a structured +# entry that pins it to specific slugs and/or section anchors. + +goals: + - id: gelfand-naimark-theorem + description: >- + Every (possibly non-unital) C*-algebra embeds isometrically as a + *-subalgebra of B(H), realized as a direct sum of GNS reps. + declarations: + - gelfand_naimark_theorem + - GNS.DirectSum.directSumAlgHom_injective + - GNS.DirectSum.directSumAlgHom_isometry + concepts: + - name: GNS representation + sources: + - { slug: "92737", anchor: { definition: GNSRepresentation } } + + - id: gns-construction + description: >- + Cyclic representation (π_ω, H_ω, Ω_ω) with + ω(a) = ⟨Ω_ω, π_ω(a) Ω_ω⟩ for any state ω on a C*-algebra. + declarations: + - GNS.Representation + - GNS.Representation.unique_up_to_unitary_equivalence + - GNS.Construction.isFaithful_iff_separating + concepts: + - name: GNS representation + sources: + - { slug: "92737", anchor: { definition: GNSRepresentation } } + + - id: von-neumann-bicommutant + description: >- + Hard half of the bicommutant theorem: every WOT-closed (or + SOT-closed) unital *-subalgebra A of B(H) equals its double + commutant A″. + declarations: + - WOTClosedSubalgebra.doubleCommutant_eq_of_isWOTClosed + - SOTClosedSubalgebra.doubleCommutant_eq_of_isSOTClosed + - SOTClosedSubalgebra.isWOTClosed_of_isSOTClosed_starSubalgebra + + - id: von-neumann-entropy + description: >- + S(ρ) = −Tr(ρ log ρ) on finite-dimensional density matrices, plus + non-negativity, the dimension bound S(ρ) ≤ log(dim), and concavity + in ρ. + declarations: + - Matrix.vonNeumannEntropy + - Matrix.vonNeumannEntropy_nonneg + - Matrix.vonNeumannEntropy_le_log_dim + - Matrix.vonNeumannEntropy_concave + + - id: umegaki-relative-entropy + description: >- + Umegaki relative entropy D(ρ‖σ) = Tr ρ (log ρ − log σ) on EReal + so non-overlapping support is admitted as +∞. + declarations: + - Matrix.relativeEntropy + - Matrix.relativeEntropy_nonneg + - Matrix.relativeEntropy_eq_zero_iff + + - id: strong-subadditivity-region-explicit + description: >- + S(ρ_AB) + S(ρ_BC) ≥ S(ρ_ABC) + S(ρ_B) for tripartite finite + tensor products. Currently region-explicit on a fixed `LocalNet` + with concrete Finset regions. + declarations: + - DensityMatrix.vonNeumannEntropy_SSA + concepts: + - name: localNet + sources: + - { slug: "92737", anchor: { definition: localNet } } + - Lieb concavity + + - id: lieb-concavity + description: >- + Joint concavity of (A, B) ↦ Tr(A^p K† B^(1−p) K) on positive + semidefinite matrices for 0 ≤ p ≤ 1 (Effros' matrix-convex + argument). + declarations: + - Matrix.lieb_joint_concavity_semidef + - Matrix.lieb_joint_concavity_rect_semidef + + # Open TODO surfaced in the README itself. + - id: strong-subadditivity-abstract-local-net + description: >- + TODO. Abstract SSA over a generic local net of algebras (currently + only the region-explicit form is formalized). + declarations: [] + concepts: + - name: localNet + sources: + - { slug: "92737", anchor: { definition: localNet } } + - name: quasiLocalAlgebra + sources: + - { slug: "92737", anchor: { definition: quasiLocalAlgebra } } + - name: local algebra A(O) + sources: + - { slug: arxiv-2507.00900, anchor: { section: "1.2" } } + - name: Tomita-Takesaki modular operator + sources: + - { slug: arxiv-2507.00900, anchor: { section: "2.1" } } + - name: KMS condition + sources: + - { slug: arxiv-2507.00900, anchor: { section: "2.1" } } + - name: Araki-Uhlmann relative entropy + sources: + - { slug: arxiv-2507.00900, anchor: { section: "2.4" } } From 140f81ececa51dde9a8f711466bcddac093f2f14 Mon Sep 17 00:00:00 2001 From: suzuki <casek2703@gmail.com> Date: Mon, 4 May 2026 17:00:22 +0000 Subject: [PATCH 5/5] chore: track skill reference docs --- .../references/output-format.md | 119 ++++++++++++++++++ 1 file changed, 119 insertions(+) create mode 100644 .claude/skills/web-to-knowledge/references/output-format.md diff --git a/.claude/skills/web-to-knowledge/references/output-format.md b/.claude/skills/web-to-knowledge/references/output-format.md new file mode 100644 index 0000000..42aff66 --- /dev/null +++ b/.claude/skills/web-to-knowledge/references/output-format.md @@ -0,0 +1,119 @@ +# Output format: `references/<slug>/` + +Per-page layout produced by `scripts/fetch.py`. Matches the +`pdf-to-knowledge` output contract so `update_concepts.py` can treat PDF +and web sources uniformly. + +## Directory layout + +``` +references/<slug>/ +├── INDEX.md # metadata + scaffolded Summary / Key concepts / External links + ToC +├── content.md # full page Markdown with preserved LaTeX math +└── assets/ # downloaded images referenced from content.md (only present when the page has images) +``` + +Exactly `INDEX.md` and `content.md` always exist. `assets/` is created +only when at least one image was downloaded. + +## Slug derivation + +- Wikipedia (`en.wikipedia.org/wiki/<Title>`) → + `wiki-<kebab-title>`. Hyphens and underscores unify, en-dashes collapse + (e.g. `Tomita–Takesaki_theory` → `wiki-tomita-takesaki-theory`). +- nLab (`ncatlab.org/nlab/show/<title>`) → `nlab-<kebab-title>` + (e.g. `relative+entropy` → `nlab-relative-entropy`). +- Everything else → `web-<basehost>-<path-basename>` + (e.g. `docs.python.org/3/library/pathlib.html` → + `web-python-pathlib`). +- `--slug` flag always wins. + +## `INDEX.md` structure + +```markdown +--- +title: "Page title" +source: "<original-url-given-to-the-tool>" +final_url: "<final-url-after-redirects>" +slug: <str> +assets: <int> +formulas: <int> # count of LaTeX math spans recovered from the HTML +--- + +# <title> + +## Summary +<!-- 3-5 sentences, filled in by Claude --> + +## Key concepts +<!-- bullet list; each bullet MUST start with `backtick-quoted` identifier --> + +## External links +<!-- optional: adjacent articles / related pages an agent may want to ingest next --> + +## Contents +- [Full content](content.md) + - [<H2 title>](content.md#<anchor>) + - ... +``` + +Frontmatter is plain YAML — machine-readable. The body is +human/agent-readable navigation. `Summary`, `Key concepts`, and +`External links` are scaffolded as `<!-- TODO -->` blocks; Claude replaces +them when filling in the workflow step 4. + +### ToC + +Always `- [Full content](content.md)` followed by indented entries for the +page's `##`/`###` headings (up to 30) with GitHub-style anchor fragments +(`content.md#foo-bar`). + +## Math handling + +- `<span class="mwe-math-element">` (Wikipedia wrapper): the MathML child + is parsed for `<annotation encoding="application/x-tex">TeX</annotation>` + or `alttext="TeX"`. The whole span — including the fallback `<img>` — + collapses to a single `$...$` / `$$...$$`. +- `<math display="block">` and plain `<math>` (nLab, some pages): same + parsing. +- `<img class="mwe-math-fallback-image-{inline,display}" alt="TeX">`: + handled as a last resort (for pages that do not inline MathML). +- MathJax `<script type="math/tex">...</script>` and + `<script type="math/tex; mode=display">...</script>`: extracted. +- `{\displaystyle ... }` wrappers injected by Wikipedia's MathML renderer + are unwrapped so the emitted LaTeX reads naturally. + +If a page appears to render math entirely client-side (no `<math>` / no +`math/tex` scripts), the `formulas` count drops to 0; the conversion still +succeeds for the prose but formulae are lost. + +## Image handling + +- Every `![alt](src)` in the generated Markdown triggers a fetch. `src` is + URL-joined to the page's final URL to resolve relative links. +- Images save to `assets/<slugified-stem>.<ext>` (max 60 chars). Collisions + are disambiguated with `-1`, `-2`, etc. +- Inline `data:` URIs are dropped — they usually represent small icons + (bullets, separators) that agents do not care about. +- Supported extensions: `.png`, `.jpg`, `.jpeg`, `.gif`, `.svg`, `.webp`. + Anything else is written with `.img` extension and still referenced, + but agents should check content-type manually. + +Image download failures log a warning and leave the original `src` URL in +place, so the conversion never aborts mid-run because of a dead CDN. + +## Cross-document concept index + +`web-to-knowledge` does **not** ship its own `update_concepts.py`. The +`pdf-to-knowledge` script is source-agnostic — it scans every +`<slug>/INDEX.md` under the references root regardless of whether the +slug originated from a PDF or a web page. Run it once after any new +ingestion: + +```bash +python3 .claude/skills/pdf-to-knowledge/scripts/update_concepts.py references/ +``` + +The resulting `references/CONCEPTS.md` groups bullets from papers and +wikis under unified concept headers, which is the whole point of the +shared output shape.