从希尔伯特纲领到 AI 证明机器：计算机科学家为何反对放弃阅读 AI 生成的代码

在希尔伯特提出"证明机器"构想一百年后，AI 智能体结合 Lean 等证明助手正将其变为现实，对数学界的冲击远超当年希尔伯特纲领的失败。作者指出，计算领域正出现"不再阅读 AI 生成代码"的风气，而程序通过 Church-Howard 对应即等同于证明，这与数学家面对 AI 生成 Lean 证明时坚持化简理解的态度形成对照。