Rocq 形式化验证:皮亚诺算术证明「K230 停机当且仅当 ZFC 不一致」

burny_tech · x · 2026-10-24

Elliot Glazer 更新了其代码库，加入了一个经典 Rocq(Coq)验证，证明皮亚诺算术(PA)能证明「K230 停机当且仅当 ¬Con(ZFC)」。这是一个纯存在性命题，从判定性语句中提取出 PA 证明仍需大量算力。

Peter Scholze 转发并点评：这是他在 Rocq/Lean 中多年来想看到的成果——一个需要两层元理论的命题，即「CiC 相信 [PA 相信某个命题]」。通常元元理论层可以消去，因为元理论证明可以被展开直接检验，但这次 Elliot 的元元理论证明基本是非构造性的。没人怀疑 PA 能直接相信最终命题，但作为演示仍非常有趣。