精益是否增强了证明可测量性？答案

【问题标题】：Does lean enhance proof surveyability?精益是否增强了证明可测量性？
【发布时间】：2020-08-30 15:59:09
【问题描述】：

通过证明可调查性，我理解人类用户可以“追踪”证明的所有细节这一事实。有些事情不容易追踪。例如，SMT 证明基于特定的启发式，然后将其转换为证明者。在这种情况下，使用简单的机制（无需成为专家即可使用它们）来扫描证明失败的原因或检查证明过程的内部结构可能很有用。

我想知道与 Coq 或 Isabelle 相比，Lean 是否增强了这种证明可调查性。通过用于形式验证的元编程框架，我得到的印象可能是这种情况。

【问题讨论】：

嗨，也许，可以考虑添加更多标签，如“smt”、“coq”、“z3”等。根据我的看法，精益也与 z3 有点相关。这可能会让更多人回答您的问题。
您可能低估了 SMT 求解器的复杂性。但是，如果您找到了一种表示 SMT 求解器（甚至是 SAT 求解器）搜索状态的好方法，请告诉我。即使它仅供专家访问。很多人都试过了。到目前为止没有成功。
而精益与z3无关，主要开发者除外。这是计划好的......

标签： z3 coq isabelle smt lean

【解决方案1】：

如果我正确理解 proof-surveyability 或 -traceability，那么根据定义，完整详细的证明是“100% 可追溯”，而仅说明结果（例如引理）是“0% 可追溯”。

在这种情况下，我不明白为什么 Lean 会比 Coq 或 Isabelle 或任何其他核心目的是检查完整详细证明的正确性的工具有所改进。此类工具通常提供增加自动化的方法，这很方便，但可以说会降低可追溯性，具体取决于如何表示额外的证明步骤。例如。类似 Coq 的策略可以提高自动化程度，但可以“恢复”可追溯性，因为该策略推断的步骤可以以与明确提供的步骤相同的方式表示：作为证明规则应用程序或推导步骤。

后半部分对于 SMT 推断的证明步骤是困难的：与 Coq 等证明检查器相比，SMT 求解器可以实现更高程度的自动化，但是以可追溯性为代价，因为它的“推理”更具技术性并且不那么像人类/演绎。

附带说明：证明检查器和 SMT 求解器之间的这种差异让我想起了经典图像识别和基于 AI 的图像识别之间的差异。前者自动化/效率较低，但更容易追踪/解释。

【讨论】：