精益提高了证明的可测量性吗？

问题描述

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

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

解决方法

如果我正确理解证明的可测量性或可追溯性，那么根据定义，完全详细的证明是“ 100％可追溯的”，而仅说明结果（例如引理）是“ 0％可追溯的”。

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

对于SMT推导的证明步骤，后一部分比较困难：与Coq等证明检查器相比，SMT求解器可以实现更高的自动化程度，但以可追溯性为代价，因为其“推理”技术性更高而不像人一样/演绎。

作为一个补充说明：证明检查器和SMT求解器之间的这种差异使我想起了经典图像识别和基于AI的图像识别之间的差异。前者自动化程度较低/效率较低，但更易于跟踪/解释。