从希尔伯特纲领到 AI 证明机器：计算机科学家为何不应放弃阅读代码

希尔伯特百年前提出的"证明机器"设想，正以配备 Lean 等证明助手的 AI 智能体形式成为现实，对数学界的冲击远超其纲领失败本身。作者以计算机科学家身份警告，如今不读 AI 生成代码已成常态，而程序通过 Church-Howard 对应即是一种证明，这与数学家不读 AI 生成的 Lean 证明同理。他主张用抽象、重构和更高层语言把代码简化到可理解，否则放弃思考将让人失去对自身命运的掌控。