AI 做数学的真相：Lean 形式化验证才是主角，AI 只是盲件

gerardsans · x · 2026-10-31

这是关于「AI 能否做数学」的争论。被回复方指出：直到最近，「AI 做数学」指的还是解有已知答案的奥数题，2025 年 7 月 AI 已达金牌水平；今年战场转向了开放问题，而「AI 缺乏创造力」的批评者在 9 月被 OpenAI 关于 Navier-Stokes 方程的内部模型结果反驳。

gerardsans 进一步纠正误解：在真实的数学研究中，专家给出的初始问题表述才是关键，配合形式化验证引擎 Lean 来验证中间和最终结果——AI 在这条流水线里只是一个「盲组件」（blind component），并非独立创造数学。