通过证明可调查性，我理解人类用户可以“追踪”证明的所有细节。有些事情是不容易追踪的。例如，SMT 证明基于特定的启发式方法，然后将其转换为证明者。在这种情况下，拥有简单的机制(不需要是专家就可以使用它们)来扫描证明失败的原因或检查证明过程的内部结构可能会很有用。
我想知道与 Coq 或 Isabelle 相比，Lean 是否增强了这种证明的可调查性。我的印象是，浏览用于形式验证的元编程框架可能就是这种情况。
最佳答案
如果我正确理解证明可调查性或可追溯性，那么根据定义，完整详细的证明是“100% 可追溯”，而仅说明结果(例如引理)是“0% 可追溯”。
在这种情况下，我不明白为什么 Lean 会比 Coq 或 Isabelle 或任何其他其核心目的是检查完整详细证明的正确性的工具有所改进。此类工具通常提供提高自动化程度的方法，这很方便，但可能会降低可追溯性，具体取决于附加证明步骤的表示方式。例如。类似 Coq 的策略可以提高自动化程度，但可追溯性可以“恢复”，因为该策略推断的步骤可以用与显式提供的步骤相同的方式表示:作为证明规则应用或演绎步骤。
后一部分对于 SMT 推断的证明步骤来说是困难的:与 Coq 等证明检查器相比，SMT 求解器可以实现更高程度的自动化，但代价是可追溯性，因为它的“推理”更具技术性并且不太像人类/演绎。
顺便说一句:证明检查器和 SMT 求解器之间的区别让我想起了经典图像识别和基于人工智能的图像识别之间的区别。前者自动化/效率较低，但更容易跟踪/解释。
关于z3 - 精益是否增强了证据的可调查性？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/63659340/