博主称Lean4无公开一致性证明，质疑AI形式化验证信任基础
Milo Moses指出Lean4缺乏相对于ZFC的一致性证明，且存在内核漏洞，提醒社区警惕对AI生成形式化证书的盲目信任。
重要性实质性证据E2 未复现写法快讯
Lean4目前缺乏相对于标准集合论公理（ZFC）的公开一致性证明。
背景：随着AI越来越多地用于生成数学证明和代码验证证书，Lean4作为核心工具被寄予厚望。然而，其基于依赖类型理论的设计追求编译速度，导致递归能力极强，使得传统的一致性证明策略失效。
结论：作者Milo Moses在LessWrong发文称，截至2026年10月，没有公开证据表明Lean4与ZFC一致。他引用Lean创始人Leo de Moura的话，承认内核中不断发现新的声音性bug（如#14576及后续七个），并指出AI擅长利用这些漏洞。
边界：此为个人博客观点，非官方审计结果。文中提到的“True=False”可被接受的风险为作者自估概率，摘要未说明测试是仿真还是实机。