AI 时代的数学危机：当形式化证明不再需要数学家

varjag · hn · 2026-08-02

文章探讨了 AI 辅助形式化验证工具（如 Lean）对数学研究的深远影响。随着大语言模型逐渐掌握将自然语言数学证明转化为机器可验证代码的能力，传统数学家在证明过程中的核心地位正受到挑战。

作者指出，这种转变虽然能消除人为错误并加速复杂定理的验证，但也引发了关于数学直觉、创造力和理论构建的哲学担忧。未来数学的发展可能不再仅仅依赖人类的灵感，而是走向人机协作甚至由 AI 主导的新范式。