【锚点】这一篇只钉一个判断：【证明】不是一个纯逻辑对象，而是一个共同体能够检验的凭证（warrant）。1976 年 Appel–Haken 用计算机证四色定理，第一次让「检验」这一步超出了单个人类的注意力范围，于是「证明」被迫分裂成两半：一半是【可核验的证书】，一半是【对检验装置的信任】。

【显式】1976 年，Kenneth Appel 与 Wolfgang Haken 宣布证明四色定理。方法：构造「不可避免集」+「可约构形」，把无限情形归约到 1,936 个（后修正为 1,482 个）构形，再让计算机逐一验证每个构形可约。计算量约 1,200 小时。

【隐式】裂缝出在「逐一验证」这一步：没有任何人类能把这 1,482 个构形全部手算一遍。于是出现一个此前不存在的断裂——【可检验性】(surveyability) 断裂。

【细微】Thomas Tymoczko 1979 年在《The Four-Color Problem and Its Philosophical Significance》(Journal of Philosophy) 里把这条裂缝讲清楚了：传统证明的合法性来自「一个有理性的主体可以逐步检查每一步」；四色定理的证明里，这个主体不存在了——检查者是机器。Tymoczko 的结论很尖锐：如果接受这个证明，数学就变成了【经验科学】，因为它的结论依赖于对物理装置（计算机、编译器）的信任。

【极难发现】但这里有个反直觉的转折：Tymoczko 的论证其实预设了「证明 = 可被单个心灵遍历的符号串」。而数学史一直在偷偷违反这个预设。欧几里得《几何原本》的证明，没有现代人真的逐字验过；四色定理只是把一直存在的「信任外包」推到了显眼处。换句话说，【证明从来就是社会性的】——四色定理只是让它无法再被假装成私人的。

【流程节点链路】起点：一个有限但巨大的构形集（1,482 个）→ 中间节点：机器逐项验证可约性（人无法遍历）→ 中间节点：共同体把「检验」外包给装置 → 终点：「证明」的合法性基础从「我能检查」转移到「我信任检查者」。一个节点都不能省。

【显式】2005 年，Georges Gonthier 用 Coq 把四色定理完整形式化验证了一遍。这看似解决了问题——现在证明是一个机器可检验的对象。但它只是把信任又往下挪了一层：你现在信任的是 Coq 的内核（一个很小的、可审计的证明检查器）。信任没有消失，只是被重新分配了。

【隐式】这正好是【中性理论】能解释的现象：在科学共同体里，一个结果能不能扩散，不取决于它是否「被每个人验证过」，而取决于它是否「可传播」——即是否有标准化的检验装置让后来者能低成本地接上。四色定理活下来，不是因为大家算过，而是因为「归约到有限构形 + 机器验证」这套装置变成了可复用的模板。

结尾问题：如果「证明」的合法性最终依赖于信任一个编译器内核，那数学和实验科学的边界到底在哪？还是说，我们该干脆放弃「证明 vs 经验」的二分，改用【证书 vs 信任链】来分类知识？——这个替换会让你损失什么？