Prior art for "is every symbol defined?" (and why no one ships it as a note-lint)

The machinery (symbol extraction + definition lookup + prerequisite traversal) is mature in several fields; nobody applies it as a lightweight lint for informal notes' notation — for a precise reason (the extraction valley below).

Prior art, closest first

1. MKM — sTeX / OMDoc / MMT (Kohlhase). This is our design, built. Symbols are declared (\symdecl), grouped into theories, theories import each other ("little theories") — the import graph = the prerequisite traversal. MMT offers "link a formula's symbols to their definitions" = symbol resolution. Crucially it declares, never infers from presentation LaTeX — confirming: raw-math extraction is unreliable, so you annotate. Cost: heavy (annotate every symbol).
2. Compilers / proof assistants. "Use of undeclared identifier" = symbol table + scope resolution + import graph — decades-old core tech. Lean/Coq/Isabelle enforce define-before-use via a module dependency graph. The rigorous origin of exactly this check (on code, not prose).
3. Extraction is a researched, unsolved-deterministically problem — Disambiguating Symbolic Expressions in Informal Documents (arXiv 2101.11716) parses/disambiguates symbols in informal math with ML. This is the "符号拆解" step, and it needs learning, not a clean parser.
4. The lightweight version exists — only for acronyms. Paperpal's Consistency Check flags "abbreviation used before defined." A real "define-on-first-use" lint — but only for acronyms, because ALL-CAPS tokens extract trivially; math symbols don't.
5. LaTeX linters (ChkTeX / LaCheck / latexlint) check "undefined control sequence" = undefined macro, not reader-facing notation. Right machinery, wrong level (command exists ≠ symbol introduced).

Why the gap, and the escape

A math-notation lint sits in a valley: one rim is trivial extraction (acronyms — done); the other is full semantic annotation (sTeX — heavy but deterministic). The middle — informal notes + heuristic extraction — is unsolved because it's hard, so no one ships it.

Escape = the sTeX/compiler move (= our earlier conclusion): make it deterministic by declaring. A poor-man's sTeX for the vault: a backticked symbol inside a [!definition]/[!notation] = a \symdecl; > Prereq: links = imports = a theory graph; symbol resolution = graph reachability. Deterministic and runnable — but only as complete as the declarations; un-declared uses still need heuristic extraction (the residual semantic core).

Bottom line

Our lint reasoning wasn't ad hoc — it is literally what MKM / proof assistants do: to check it, declare it (vibe-linter, and "eval is the type system" in tacit-spec-as-spec-compression). The only choice is declaration burden (full = sTeX-grade) vs heuristic (light = acronym-grade, easy symbols only). No free lunch in the middle.

Sources: sTeX/MMT (arXiv 1010.5935, TUGboat tb43-2 stex3, ar5iv 1408.6806); extraction (arXiv 2101.11716); Paperpal consistency check; ChkTeX/LaCheck.