Wir müssen wissen – wir werden wissen

remywang主张，即使AI生成的代码通过测试或形式化验证，计算机科学家也不应放弃阅读和理解代码。文章从Hilbert计划及Gödel、Turing的不可能性结果谈起，将配备Lean等证明助手的AI智能体与自动证明的理想联系起来。数学家会简化过长的AI生成证明，计算领域也应通过抽象、重构、缩小范围和采用更高层语言，让代码保持在人能理解的范围内。