AI 证明定理后，我们为何不再阅读代码？
Wir müssen wissen – wir werden wissen
一百年前，David Hilbert 曾梦想构建一个能自动判定所有数学真理的完备系统，却被 Gödel 和 Alan Turing 证明为不可能。然而讽刺的是，正是这些证明催生了计算机科学，而今天的 AI 正借助 Lean 等工具实现 Hilbert 的“证明机器”。作为计算机科学家，我深感忧虑：当 AI 生成的代码或证明过于复杂时，我们是否正在放弃阅读和理解？在数学界，人们会努力简化长证明以维持理解；但在编程领域，我们却开始默认接受 AI 生成的黑盒代码。这种放弃思考的趋势是场悲剧，因为程序即证明，放弃阅读代码等同于放弃对科学本质的掌控。
对于愚昧的‘不可知论’，我们的口号应当是：我们必须知道——我们将知道。
HN 评论区
15- dragontamer
> 反对那愚蠢的“我们永远无法知晓”（ignorabimus），我们的口号应当是“我们必须知晓——我们将要知晓”（Wir müssen wissen – wir werden wissen）。
对于想更快看到译文的朋友。恕我直言，把标题的含义和整篇博客的核心论点拖到第 7 段才讲，有点不公平。
- t0mek
> 我们在计算领域也必须持同样的态度：使用抽象、重构、细化范围、发明并采用更高级的语言，直到我们能把代码装进脑子里。
我希望这是真的。但作为一个反例，我们需要把 C 或 Golang 程序生成的机器码或汇编代码装进脑子里吗？或者说，Golang 代码本身就是一种足够好的高级抽象？
如果是这样，这是否意味着我们应该走得更远，把设计文档视为适合装进脑子里的“代码”，而把 Golang 程序视为其衍生物？或者也许设计文档也太低阶了，那种“给我造个应用，别出错”的通用氛围其实就足够了？
正确的抽象层级是什么？该如何找到它？
- user2342
"必须知晓！"