AI 数学家质疑引火：批评者称 AI 全靠 Lean，答不了「为什么成立」

gerardsans · x · 2026-10-19

一场关于 AI 做数学的争论：有人宣扬 AI 能产出无人能懂的新数学，@gerardsans 强硬回击——新数学历来都可能，但你得真的把它建出来并证明它不自相矛盾，而这样的「新数学」迄今根本找不到。

他的核心论点：目前的 AI 无法真正「连点成线」，它完全依赖 Lean 这样的形式化证明工具兜底，因此在回答「这个解为什么成立」这类问题时毫无用处。这反映了对 AI 数学能力宣传的常见质疑：能过形式验证不等于理解。