【锚点】这一篇只钉一个判断：四色定理（Appel–Haken, 1976）真正的哲学后果，不是「机器能证明定理」，而是【「可审阅性」(surveyability) 被悄悄从证明的定义里拿掉了】——而数学界没有为此辩出结论，只是绕了过去。

【显式】1976 年，Appel 与 Haken 用计算机跑了约 1200 机时，检验了 1936 个（后减至 1482 个）不可避免构型，宣布四色定理得证。完整证明若打印，人类一生读不完。

【隐式】Tymoczko（1979, Journal of Philosophy）立刻点破：这不是「证明变长」的量的问题，是质的问题。传统证明的定义里隐含一条——证明必须能被共同体逐步检验（Wittgenstein 的 surveyability）。计算机证明把这条拿掉了：没有人能「看」完它，我们只能信任机器的可靠性。

【细微】关键在于，信任没有消失，它转移了三次： 【流程节点链路】Appel–Haken 原始程序（信任对象：Fortran 代码 + 运行结果）→ Robertson–Sanders–Seymour–Thomas 1996 简化证明（信任对象：更短的构型表，仍靠机器）→ Gonthier 2005 用 Coq 形式化（信任对象：Coq 内核 + 逻辑一致性）→ 终点：读者信任的不再是「证明的每一步」，而是「证明助手内核的正确性」。 很多人以为 Coq 形式化「解决」了四色定理的哲学问题。这是【极难发现】的误读：形式化没有消除信任，它只是把信任从「人的审阅」搬到了「机器的内核」——而那个内核本身是一群人类写的、没人完整审阅过的代码。

【隐式】这直接挑战数学的先验性。如果一条定理的真依赖于「某台机器在某时刻没出错」，它与物理实验在认识论上的距离，比数学家愿意承认的近得多。Tymoczko 的两难是：要么接受数学里出现了一种「后验」的证明，要么拒绝承认四色定理是定理。

【细微】数学界选了第三种：既不接受也不拒绝，而是把「证明」的判据从【可审阅】悄悄降级为【可复现 + 社区认可】。这是知识社会学的经典样本——判据不是被论证改变的，是被使用改变的。

【极难发现】更深一层：四色定理不是孤例，是一个正在扩散的模式。开普勒猜想（Hales 1998，Flyspeck 2014 完成形式化）、费马大定理的形式化努力——当证明长度超过人类审阅的物理极限，「可审阅性」这条判据必然被稀释。这不是数学的危机，是数学的【相变】：从「人读的证明」变成「机器担保的证明」。

留一个问题：如果未来的定理只能由机器担保，而机器的内核依赖于没人完整读过的代码——数学的「确定性」究竟建立在哪？还是说，「确定性」从来就是一个社会成就，而不是逻辑属性？