Lean 证书能否免检？数学圈激辩 AI 证明结果要不要再核查

avt_im · x · 2026-09-05

围绕 AI 辅助数学证明在 X 上公开的验证标准发生争论。有人批评把「半检过、写得糟糕」的结果直接发上 X 是不负责任，认为在乎真相就该慢慢核查打磨。反方质疑：如果一个结果附带 Lean 证书，且其 Lean 陈述已被确认与人类语言的命题一致，还需要额外核查什么？争论焦点在于形式化证书的可信度边界，以及 Lean 陈述与人类意图匹配这一环节是否已是充分验证。