数学定理就是一张保修卡。结论是正面那行大字，适用条件是背面的细则——人类读教材时脑子会自动补上细则，AI 不会，它逐字执行。少一条细则，索赔就该被拒；更糟的情形是连被拒都不会发生：AI 拿着残缺的保修卡宣布索赔成功，而没有人发现。FARMS 干的就是这件事：把四本经典教材里 171 个形式化目标，一条不漏翻成机器能查的 Lean 4。
补漏 1：空真——自动证明的头号敌人
一个条件语句当前提根本没有为真的实例时，就空洞地真。「所有独角兽都是白色的」——真，因为独角兽不存在。日常里是段子，计算保证里是陷阱。FARMS 抓出的具体版本：随机低秩逼近定理里藏着一个前提——算法得真的能输出合法结果。对比系统丢掉了「输出存在」，只保留误差条件。后果：如果算法在某些输入上根本构造不出合法输出，全称量词扫过空集，保证自动为真，系统宣布形式化成功——成功是假币。计算保证的全部用途是安抚一台正在运行的机器，在算法跑不出结果的输入上自动生效的保函就是白纸。虚假的成功比诚实的失败危险得多——失败至少会叫出声，空真是静音的。
补漏 2：两行小字，编译器一声不吭
案例一发生在低秩逼近定理上。初始候选编译通过，眼看过关，语义评审员拦下两处。情形一：A 是零矩阵、k 取 1 时不存在合法输出——漏掉的是秩限制。情形二更阴：n 取 1 时参数整个消失，源文本的 log 无定义，而 Lean 顺手定义了 log(0) 等于 0，编译器把未定义当 0 静默放行。一个公式在定义域之外的点被悄悄赋值，像给过期保修卡盖了有效章。抓它们只能靠语义评审——一个较真的角色对着原文问：你的意思是这个吗。编译器帮不上忙，它只管语法良好。
补漏 3：五十年后，教材被自己的学生逮个正着
案例二是全文高潮。教科书说：按范数加权采样的分布能最小化期望平方误差，且对一切可容许分布最优。形式化器忠实保留原文声明的域（允许某些分量取零），编译通过。语义评审员构造了一个能写在手背上的反例：A 等于 [1,1]，B 等于 [1,-1]，只取一个样本。精确乘积是 0。「最优」分布的期望平方误差是 4；一个故意只抽第一项的可容许替代分布，误差是 1。号称对一切最优的分布，4 大于 1，输得干净利落。病根：无偏性论证需要「每个非零贡献的采样概率必须为正」——原文缺了这条。这回错的是教材本身，claim 在文献里躺了五十年被一代代读者默认成立，直到一台机器在翻译它的时候顺手审计了一遍。流水线的处置很有分寸：保留原样，缺失条件记为显式源警告，本次运行记为未接受——原厂出品带着公示瑕疵的保修卡，和被悄悄换过内芯的，必须可区分。
补漏 4：较真反而便宜二十倍
171 个目标 157 个接受，91.8%；其余诚实弃权、理由记录在案。成本侧：在 6 个随机目标上，FARMS 总计 17.06 美元、227.5 万 tokens；对照的 brute-force 式系统烧掉 348.09 美元、6307 万 tokens——每个目标 2.84 美元对 58.02 美元，差 20.4 倍。便宜从哪来：把力气花在刀刃上，检索器按需回原文取证，语义评审把「编译能过但意思不对」的候选在早期拦下，补不上的缺口不再无限续命。每一次较真都发生在最便宜的时刻。文末两个技能化应用值得点名：热流求解预条件后条件数 8.83 到 8.95，比标准对角预条件的 99.6 到 964.0 好一到两个数量级，6 次运行全部 22 次迭代内收敛；弦的波响应压缩，残差界 0.00877 到 0.00938 压在 0.01 目标之下，32 个时间步的响应库从 24 MiB 压到 8.375 MiB，且能量守恒把初始误差的界直接带到所有未来时刻——一纸保函覆盖全程。
下一根钉子：RNLA 和数值 PDE 是两个领域，171 个目标的覆盖外推性有限；每目标两美元是估计成本，真实大规模跑起来检索和评审的方差有多少；以及那条源警告能不能被教材下一版收录——机器给人类知识开的体检报告，作者认不认。
边界一条：这是三部曲的第二篇——第一篇 AWM 立法，这一篇公证。公证员的工作是把已有法律登记入册，它不生产新数学。157 个接受是「忠实翻译并机器可查」，不是「171 条定理都被重新证明了一遍」——定理本身还是原样躺在那里，变的只是保修卡的背面从「大家默认懂」变成了「逐条可验证」。