理论计算机科学家 Fortnow：AI 补全证明细节的速度超预期

计算理论学者 Lance Fortnow 表示，AI 接手研究论文、补全形式化证明细节并验证证明的进展速度超过其预期。他 2022 年在 CACM 写文章时曾认为这一任务仍很遥远，如今感叹自己的“梦想得不够大”。Lean 等形式化数学工具与 LLM 的结合，正快速推动数学证明自动化。