「每个符号是否都已定义」的既有方案（以及为什么没人把它做成笔记的轻量 lint）
这套机器（符号抽取 + 定义查找 + 前置知识遍历）在好几个领域里都已经成熟；却没有人把它用作非正式笔记记号的轻量级 lint —— 原因很明确（见下文的"抽取谷"）。
既有方案，从最接近到最远
- MKM —— sTeX / OMDoc / MMT（Kohlhase）。 这正是我们的设计，而且已经有人做出来了。 符号被声明（
\symdecl），归入理论（theories），理论之间彼此导入（import）（"小理论"思路）—— 导入图就是前置知识遍历。MMT 提供"把公式里的符号链接到其定义"的功能，也就是符号解析。关键是它始终在声明，从不从排版 LaTeX 里反推——这印证了一点：从原始数学式里抽取符号是不可靠的，所以才要靠人工标注。代价：重（每个符号都要标注）。 - 编译器 / 证明助理。 "使用了未声明的标识符"这类报错，背后就是符号表 + 作用域解析 + 导入图——几十年历史的核心技术。Lean / Coq / Isabelle 通过模块依赖图强制"先定义后使用"。这正是我们这个检查的严谨源头（只不过它检查的是代码，不是散文）。
- 抽取本身是一个已被研究、但无法判定式求解的问题—— Disambiguating Symbolic Expressions in Informal Documents（arXiv 2101.11716）用机器学习来解析/消歧非正式数学文本里的符号。这正是"符号拆解"这一步，它需要学习，而不是一个干净的解析器就能搞定。
- 轻量版是存在的——但只针对缩写词。 Paperpal 的 Consistency Check 会标记"缩写在被定义之前就使用了"。这是一个真正的"首次出现即定义"式 lint——但只适用于缩写词，因为全大写的 token 抽取起来毫无难度；数学符号做不到。
- LaTeX 检查工具（ChkTeX / LaCheck / latexlint） 检查的是"未定义的控制序列"，也就是未定义的宏，而不是面向读者的记号。机制是对的，但层级不对（命令存在 ≠ 符号已被引入）。
缺口从何而来，以及出路
一个数学记号 lint 处在一个谷地里：一侧的谷壁是平凡的抽取（缩写词——已经解决）；另一侧是完整的语义标注（sTeX——重，但确定性）。中间地带——非正式笔记 + 启发式抽取——之所以没人解决，是因为它本身就难，所以没人把它做成产品。
出路 = sTeX/编译器那条路（= 我们之前的结论）：靠声明把它变成确定性问题。 给 vault 用的穷人版 sTeX：[!definition]/[!notation] 里用反引号包起来的符号 = 一个 \symdecl；> Prereq: 链接 = 导入 = 一张理论图；符号解析 = 图可达性判断。这是确定性、能真正跑起来的方案——但它的完备程度取决于声明得有多全；未被声明的用法仍然需要启发式抽取（这是剩下的语义核心难题）。
结论
我们这套 lint 的思路并非拍脑袋想出来的——它其实就是 MKM / 证明助理在做的事：要检查它，就先声明它（vibe-linter，以及 tacit-spec-as-spec-compression 里"eval 即类型系统"那一条）。唯一要做的取舍是声明的负担（完整版 = sTeX 级别）对启发式（轻量版 = 缩写词级别，只能处理简单符号）。中间地带没有免费午餐。
来源：sTeX/MMT（arXiv 1010.5935、TUGboat tb43-2 stex3、ar5iv 1408.6806）；抽取（arXiv 2101.11716）；Paperpal consistency check；ChkTeX/LaCheck。