数学家争论形式化证明新规：数学的「我们」由谁定义

jessi_cata · x · 2026-09-22

围绕 AI 时代形式化证明（Lean 等）在数学界地位的争论：发帖人指出旧规则要求接受 ZFC 框架下的证明，虽然 Lean 严格说不同于 ZFC，但这并非争论核心。有人想改规则，有人坚持现行规则——而「我们从未投票决定改变规则」。

作者批评部分数学家以「我们在乎的不是形式化证明而是那些模糊的东西」为由轻视形式化，反问这个「我们」是谁、谁的意见算数、是否经过表决。这折射出 AI 辅助形式化浪潮下数学共同体标准之争。