count-catcher

新工具将模型计数证书转换为 Lean 定理

研究人员开发了一个名为 count-catcher 的工具，该工具可将精确模型计数器 d4 的证书转换为 Lean 定理。这些定理断言，在 Lean 中定义的给定 CNF 公式在一组变量上具有特定数量的模型。该过程涉及验证等同于该公式的布尔电路及其等价性证明。该系统与 Lean 的标准库和现有的数学结果集成，能够对复杂的组合计数进行认证，例如 8 阶拉丁方块的数量。