Lean 开源外部检查器 con-leche，自身一致性获形式化证明

Lean 官方介绍了新开源的外部检查器 con-leche（CONsistent LEan CHEcker），由 Joachim Breitner 等开发。其突出特点是自身一致性在 Lean 中得到了形式化证明，即该检查器不会接受任何对 False 的证明。作为独立于 Lean 核心的验证工具，它为 Lean 证明的可靠性与可审计性提供了新的保障，也展示了元层验证方法的可行性。

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

• Lean 推出外部验证器 con-leche,在 Lean 内证明自身一致性 — AlexKontorovich · 2026-09-10
• con-leche：用 Lean 证明自身一致的外部 Lean 检查器开源 — burny_tech · 2026-09-11