标签
一篇纪念希尔伯特纲领提出一百周年的反思性文章，回顾了哥德尔不完备性定理和图灵停机问题如何使这一纲领受挫，并论证如今由 Lean 等证明助手驱动的 AI 智能体正在实现希尔伯特的“证明机器”，对数学和计算机科学产生深远影响。