LessWrong 长文：Lean4 至今没有公开的一致性证明

MoonL88537 · x · 2026-10-13

LessWrong 文章《A critical look at Lean4》指出，到目前为止没有任何公开可用的证明说明 Lean4 相对于 ZFC 加任意大基数公理是一致的。作者最初以为这只是未被写出的技术细节或 bug，但深入后的结论是：Lean4 的一致性并非「还没人费心写出来」，而是目前不知道它为什么应当一致，且所有已知证明策略都面临实质障碍。作者转推提醒：在 Lean 中被形式化证明的东西，未必就是你以为的含义——他此前也把问题误认为是若干 bug。对 AI 形式化验证和定理证明相关讨论有直接影响。