LLM让数学证明生成更快，验证成瓶颈

michaelchchoi · x · 2026-07-14

这条转发强调：随着 LLM 生成的数学证明越来越多，**验证**可能会成为新的瓶颈。原帖作者分享了自己用 LLM 辅助寻找并形式化 **Kannan–Tetali–Vempala 猜想**证明的经验，总结了若干使用心得，面向的是“AI 辅助数学证明”这一具体研究实践，而不是泛泛讨论。