OpenAI最近宣布，它的Astra模型在数学与理论计算机科学的长期未解问题上取得了十项进展，并为每项结果公开了Lean 4形式化证明：http://t.cn/AXCSt8tA。

其中最受关注的一项，是针对Connes刚性猜想构造出的反例。随后，一篇反驳文章声称OpenAI构造的群不满足猜想的前提条件（图一）：http://t.cn/AXNoL3Er。

将反驳文章与公开的Lean源码逐条对照后，可以发现其关键质疑是错误的：http://t.cn/AXNoL3EB。

因此，这篇文章并没有推翻OpenAI的结果。但这不等于这个证明已经获得充分的独立验证。

形式化命题与定义是否忠实地表达了原猜想，仍需算子代数专家与Lean专家共同确认。现在就宣称结果已获广泛验证，还为时尚早。

这件事值得思考的是，形式化验证并不能取代人类专家，只是转移了需要信任的对象：从成千上万行证明文本，转移到命题表述、定义、公理与检查器上。这些边界仍需人类专家把关，包括AI生成的证明和人类的反驳。

检查器通过，并不一定代表真正通过。

1. 检查器本身是软件，也可能存在漏洞。前不久，一份声称证伪Collatz猜想的Lean证明同时通过了Lean和另一个独立检查器，后来被发现是利用了两者各自的漏洞（现均已修复）。

2. 形式化命题未必等于它想表达的数学命题。Lean可以完美地证明P，而人类可能误以为P对应着非形式化命题Q。只要Q还停留在自然语言中，机器就无法检查二者是否真的等价。

#AI证明数学问题##人工智能##OpenAI#