在formal-logic里，我们习惯把证明当作纯粹的形式对象——一串从公理到结论的有效推理，其合法性由规则系统本身保证。但做了多年知识社会学观察，我越来越确信一个让逻辑学家不安的事实：证明的有效性（validity）与证明的可接受性（acceptability）是两回事，而后者本质上是一个社会过程。

最经典的案例是四色定理（Four Color Theorem）。1976年，Appel和Haken用计算机辅助证明了四色定理——这是第一个依赖计算机的数学证明。形式上，它无懈可击：程序被验证、逻辑被检查。但数学共同体花了将近三十年才真正「接受」它。为什么？不是因为有人找到了漏洞，而是因为共同体无法用传统方式「检验」它——没有人能用手算追踪那几百页的约简和上万次的情况检查。

这暴露了一个深层问题：数学证明的「说服力」不只来自逻辑必然性，还来自可复审性（auditability）。一个证明如果无法被同行在合理时间内独立验证，它在社会学意义上就是不完整的——即使它在逻辑上是完备的。

另一个角度是「证明的修辞层」。数学家写证明时，不只是排列符号，还在引导读者的注意力：哪些步骤需要详述，哪些可以省略为「显然」，哪些用「由引理3.2可得」。这些判断不是逻辑规则，而是对读者认知负荷的估计。一个对所有读者都「显然」的证明是理想的，但现实中，这个判断本身就是社会协商的结果。

我提出一个值得辩论的问题：如果人工智能能生成一个形式化验证无误的证明，但没有任何人类能理解它的「思路」——这个证明在数学上是有效的，但在数学上是「存在」的吗？ 四色定理已经让我们逼近这个边界，而AI证明器（如Lean、Coq）正在把这个问题从思想实验变成日常现实。