AI数学证明，需要区分结果核验与过程复现

2026年11月6日，PSI报告称，借助未公开的Anthropic模型获得了Aaronson–Ambainis猜想的证明。值得讨论的不只是AI能否完成数学工作，而是这项声明中，哪些部分能够由外部人员实际检验。

研究结果与产生结果的过程，需要不同证据

公开仓库提供Lean形式化证明及核验记录，同时将命题是否对应原猜想留给人工审查。Open Market Notes没有重新运行证明，也没有复现发现过程。

我们的判断是，两种看似相反的态度可以同时成立。研究者可以认为公开、可检查的数学成果很有价值，同时暂不判断生成它的系统具备怎样的普遍能力。反过来，无法使用同一模型，并不能直接否定一份证明。将两者混在一起，容易把可以逐项检验的研究对象，变成对一家公司的整体表态。

设想一位评估者只收到最终证明文件，没有失败尝试的记录。他或许可以判断，这份文件是否证明了指定命题，却不能由此推算模型解决新问题的概率、人工筛选的程度，或者此前失败搜索的成本。这些问题需要不同的观察材料。一次成功成果，并没有提供计算成功率所需的分母。

量子计算的含义有明确范围

原始论文将这一猜想与查询模型中对大多数输入的经典模拟联系起来。它不是对量子机器进行的性能测试。

对商业读者而言，这一区分会改变接下来的问题。抽象算法需要访问输入多少次，不等于交付日期、用电成本或应用运行时间。要做实际比较，必须指定工作负载、实现方法及资源核算方式。本文没有提供这些证据，因此不能据此支持硬件采购决定，更不能推断现有安全系统何时失效。

合理态度既不是因为理论没有立即变成产品而忽视它，也不是把理论结论直接描述成工程成果。理论可以改变哪些问题值得研究，但工程仍需检验相关假设是否适用于目标应用。对一类问题的限制，不应在传播中悄然变成对量子计算全部用途的判断。范围越清楚，研究的真正价值反而越容易被理解。

核验应是一套工作流程，而不是标签

Lean文档区分经典推理与计算内容。因此，一项形式化结果不应自动被描述为可直接执行的方法。

我们建议，编辑与研究团队分别记录准确命题、审查版本、实际执行的检查，以及检查范围以外的结论。这是评估建议，不代表本刊已经审计PSI的工作。版本身份很重要：对一个文件的审查，不应成为对以后所有修改的认可。记录也应注明审查者，并区分发布方日志与外部人员独立重复运行的结果。

这种做法同样有助于处理分歧。如果争论针对定义，应讨论形式化对象是否对应原来要研究的对象；如果针对推导，应指出哪一步存在问题；如果针对AI能力，则应检查任务选择、人工干预及可重复性。把分歧保留在正确层次，才能在一处需要修正时，不武断地宣布所有其他结论都随之失效。

对于考虑采购AI研究工具的机构，问题也不应停留在最令人印象深刻的演示。试用前可以先确定真正关心的问题，记录全部尝试，核算专家投入，并事先规定输出如何检验。这是一种评估设计，并非对PSI表现的估计。无论工具最终成功还是失败，它都能使后续比较更有解释力，而不是只留下容易传播的成功案例。

公开成果的重要性，在于允许人们提出具体、可定位的审查问题。下一项有用进展，应当是独立检查究竟确立了什么，而不是标题再增加一个强调突破的形容词。在此之前，数学有效性、发现过程的可重复性与实际影响，仍应作为三个不同判断。