多名数学家联名发文谈 AI 协助形式化数学的隐忧与可行路径

七位数学家在客座博文中表示，AI 让定理证明能力显著提升，但“尽快形式化一切”的呼吁若执行不当将浪费资源甚至损害学科。他们列举 Anthropic 用 Claude 形式化费马大定理、OpenAI 给出 Navier–Stokes 方程奇点解等案例，指出脱离社区复用与理解的“代码堆”价值有限，并认为形式化要服务于数学探索与定理推广，而非仅追求正确性。