【锚点】这篇只钉一个判断：四色定理的争议从来不是「对不对」，而是「一个无法被单个人从头到尾审视的证明，还算不算证明」。

【显式】1852 年 Guthrie 提出四色猜想。1976 年 Appel 与 Haken 在伊利诺伊大学把问题归约到 1,936 个「可约构型」，机器跑了约 1,200 小时，人工分析约 400 页。1996 年 Robertson–Sanders–Seymour–Thomas 把构型压到 633 个，仍是计算机辅助。2005 年 Gonthier 用 Coq 把整个证明形式化，机器可完整核验。

【隐式】关键不在「用了计算机」。关键在 Tymoczko 1979 年《四色问题及其哲学意义》里那个词——【可审视性 surveyability】：一个证明之所以是证明，传统上要求一个（理想化的）人能逐步检查每一步。Appel–Haken 的证明不满足这一条：没有任何人能同时握住 1,936 个构型的手工分析与几百万步机器检查。

【流程节点链路】猜想(1852) → Appel–Haken 计算机穷举(1976, 1,936 构型) → Tymoczko 的「不可审视性」质疑(1979) → Robertson 等简化(1996, 633 构型) → Gonthier 的 Coq 形式化(2005) → 信任下沉到内核。

【细微】一个被忽略的比对：四色定理不是第一个「不可审视」的证明，它只是第一个「可见的裂缝」。有限单群分类（CFSG）横跨约 100 位作者、上万页、数百篇论文，从没有一个人从头到尾读过；2004 年 Aschbacher–Smith 还补上了 quasithin 情形的一个真实缺口。也就是说，「可审视性」在四色定理之前就已经是数学共同体的一个善意虚构——只是没人愿意承认。

【极难发现】Gonthier 的 Coq 形式化常被当作「解决了可审视性问题」。它没有。它只是把信任从「1,936 个构型的手工检查」下沉到「Coq 内核 + OCaml 编译器 + 硬件 + 那套与浮点无关的逻辑」。信任链没有消失，只是变短、变硬、变得更难被一个外行质疑。这正是知识社会学里的老规律：验证的成本不会归零，它只会被重新分配。

【结论】四色定理教给我们的不是「计算机能证明定理」，而是：证明的接受从来不是逻辑的自动产物，而是一个共同体用它的【验证基础设施】做的一次审计。当基础设施从人脑换成内核，数学的「经验性」没有增加，只是换了承重墙。

【值得辩论】如果所有大证明（CFSG、Kepler 猜想的形式化、Mochizuki 的 abc）最终都只能被机器或小圈子审计，那么「数学是唯一不需要信任的科学」这句话，是不是从一开始就是个神话？