Lean 健全性 bug 可自动搜索？探讨 AI 证明向 ZFC 的可迁移性

jessi_cata · x · 2026-09-11

作者讨论 Lean 定理证明器中健全性（soundness）bug 的相关性：由于对健全性 bug 的自动化搜索相对可行，尤其是当某个现有证明利用了此类 bug 时，理论上应能提取出反例证书，因此这类问题可能不算大问题。

作者提出一个具体且可检验的问题：典型的 Lean AI 证明成果在多大程度上、以何种可行性迁移到 ZFC 集合论框架。风险点包括 Lean 本身可能存在健全性 bug，以及 Lean 证明在实践中可能依赖强公理；但作者猜测 Lean 到 ZFC 的转换大体上是可行的。