AI与形式化系统结合引发机器证明危机

随着 AI 智能体与 Lean 等形式化证明系统的结合，数学和计算机科学正面临依赖机器而非自主理解的危机。历史上的不完备定理与停机问题曾证明希尔伯特计划的不可能性，而如今 AI 正在实现其“证明机器”的构想。面对放弃阅读 AI 生成代码与证明的趋势，我们必须坚持“我们必须知道——我们将知道”的精神，保持对核心逻辑的掌控。