【发布时间】：2020-06-12 18:28:47
【问题描述】：
我有一个由 Sledgehammer 获得的 Metis 证明，以紫色突出显示。它被突出显示的确切含义是什么？证明似乎有效；真的吗？
【问题讨论】：
标签： isabelle
【发布时间】：2020-06-12 18:28:47
【问题描述】：
紫色表示metis 调用仍在运行。有三种可能的结果：
- metis 完成：证明有效（无背景）；
- metis 失败：证明无效（红色背景）；
- metis 没有终止：证明无效（紫色背景永远保留）。
Isabelle 是多线程的，只有在所有之前的策略都完成后，你才安全。
您决定等待的时间取决于您，但多于几秒钟通常意味着您必须重新运行 Sledgehammer...
【讨论】：