Lean 型理论在排除中律下可证 ZF 一致性,且结果由 AI 辅助发现

MikePFrank · x · 2026-09-23

Mario Carneiro 在 arXiv 发表论文:在 Lean 核心类型论(含经典排中律、不含任何选择公理)中,可证明 ZF 集合论的 outright 一致性,证明已在 Lean 中形式化。此前普遍认为缺少选择/描述算子会让类型论强度远低于 ZF,结果并非如此。perrymetzger 转发时指出这一结果是用 AI 发现的。Mike Frank 质疑:这只能说明 ZF 一致则 Lean 一致(反向蕴含),且 Lean 曾有可证 False 的已知 bug。论文机制依赖对可达性谓词的大消去与由命题守卫的良基树递归。