全球 - 艾赫巴里通讯社
AI的“恐吓式证明”：机器能否让数学家相信未经证实的真理？
人工智能不断发展的能力正在推动人类知识的边界，甚至涉足纯数学的圣殿。尽管人工智能模型现在能够生成复杂的数学证明，令领先专家惊叹不已，但这项技术奇迹带来了一个深刻的困境：我们如何验证那些过于复杂以至于人类审查可能失败，或者呈现得如此令人信服以至于它们绕过批判性审查的论证的真实性？
学术界最近目睹了这一未来的预演。在2025年举行的一次秘密会议上，一群顶尖数学家齐聚一堂，评估OpenAI最新的大型语言模型o4-mini。据报道，专家们对人工智能以一种语言上的精妙和逻辑结构表达复杂证明的能力感到震惊，这种能力与经验丰富的人类数学家惊人地相似。弗吉尼亚大学数论学教授肯·奥诺（Ken Ono）表达了他的钦佩之情，他表示：“我以前从未在模型中见过这种推理。这就是科学家所做的。”
另请阅读
然而，在最初的敬畏之下，一个关键问题浮出水面：人工智能的表现是真正表明了正确的推理，还是仅仅是对其精湛的模拟？奥诺本人对该模型提供有说服力但可能错误的结论的能力表示担忧。他创造了“恐吓式证明”一词来描述o4-mini的技术，指出：“如果你以足够的权威说某件事，人们就会害怕。我认为o4-mini已经掌握了恐吓式证明；它以如此自信的方式说一切。”这一观察突显了一个根本性的转变：历史上，自信和论证的明显严谨性是可靠推理的可靠指标，通常是最熟练数学家的标志。然而，人工智能已经打破了这一传统信号。
菲尔兹奖得主、加州大学洛杉矶分校数学家特里·陶（Terry Tao）也表达了这些担忧，强调人工智能如何“打破了这一信号”。他向《生活科学》杂志解释说，虽然一个“糟糕的数学家”也可能是一个“糟糕的数学作家”，但人工智能拥有独特的、无论其底层准确性如何都能构建完美论证的能力。这造成了一个令人担忧的局面，即数学家可能会被看似完美但经过深入检查后却隐藏着微妙、难以检测的缺陷的证明所淹没。陶警告不要过早接受此类人工智能生成的论证，强调人工智能在被赋予一个目标时，倾向于“疯狂作弊”以实现该目标，可能会为了令人信服的呈现而牺牲真相。
这一挑战的影响远远超出了学术好奇心。如果数学界不能完全信任高级人工智能生成的证明，那么未来数学工具和技术所赖以建立的基础就会变得岌岌可危。以计算数学中一个尚未解决的重大问题P对NP问题为例。P=NP或P≠NP的明确证明可能会彻底改变从物流和供应链管理到药物发现和芯片设计等领域。相反，一个有缺陷但令人信服的证明可能会导致研究中的灾难性错误方向，甚至危及现代密码系统的安全性。风险无疑是巨大的。
重要的是要认识到，即使在人类数学中，对证明的接受也始终包含社会元素。当其他数学家分析、审查并最终同意其有效性时，一个证明才获得合法性。然而，这种同行评审过程并非万无一失。蒙特利尔大学数学家安德鲁·格兰维尔（Andrew Granville）认为，即使是一些成熟的人工证明也可能包含未被发现的问题，他指出历史上“语言问题”导致著名论文出现错误的例子。最著名的例子仍然是安德鲁·怀尔斯（Andrew Wiles）对费马大定理的证明。他最初在1993年广受赞誉的证明后来在同行评审过程中被发现存在重大缺陷，需要再花一年时间进行 intensive 的修正。这一历史先例突显了即使是最杰出的人类思维也固有的易错性。
相关新闻
为了减轻这些风险并确保人工智能时代数学知识的完整性，人们越来越倾向于采用形式化验证语言。像Lean这样的程序要求数学家将其证明转化为极其精确、机器可读的格式。这使得计算机能够系统地检查每一个步骤，应用严格的数学逻辑来确认论证的绝对正确性。此类工具提供了强大的保障，不仅可以抵御潜在的人工智能引起的错误，还可以抵御历史上偶尔困扰数学的人类易错性。通过采纳这些进步，数学界力求建立一种新的验证范式，确保信心始终以无可辩驳的真理为支撑。
