LessWrong 长文质疑 Lean4 一致性未被证明

LessWrong 发布长文《A critical look at Lean4》，指出常被忽视的基础问题：Lean4 本身的一致性并未被证明，因此不应盲目相信「有 Lean 证明就万事大吉」。相关文章进一步列出三点质疑，包括 Lean4 底层理论缺乏完整一致性证明等基础层面缺陷，并提及基准污染问题，认为形式化证明并非银弹，仍需谨慎对待其可信度。

2026-10-11 ~ 2026-10-12 · 2 条相关