操作说明🔗

在 Lean 交互工作时，定理证明完成后，代码左侧的槽中会出现蓝色双勾。

含义🔗

蓝色勾号表示定理陈述已依据当前文件及其导入文件中定义的语法和类型类实例成功精译，并且 Lean 内核已接受一个由当前文件及其导入文件中声明的定义、定理和公理推出的该定理证明。

信任🔗

如果相信形式化定理陈述符合其预期的非形式含义，相信导入库的作者是诚实的、已检查库中定理表达了预期含义，且没有声明和使用不健全的公理，则此检查有意义。

防护🔗

备注🔗

可以在 Visual Studio Code 扩展设置中更改该符号。 非 VS Code 编辑器可能使用不同的指示方式。

运行 lake build +Module（其中 Module 指包含定理的文件），并确认成功且没有错误消息或警告，可提供相同保证。

操作说明🔗

在定理声明后写入 'thmName' does not depend on any axioms#print axioms thmName，将 thmName 替换为定理名称，并确认报告中只有内置公理 propext、Classical.choice 和 Quot.sound。

含义🔗

该命令打印定理及其依赖定理所使用的公理集合。 上面的三个公理是 Lean 逻辑的标准公理，没有危害。

• 如果报告 sorryAx，则该定理或其某个依赖使用了 sorry，或以其他方式未完成。

• 如果报告 Lean.trustCompiler，则使用了本地求值；说明见下文。

• 任何其他公理都表示声明并使用了自定义公理，此时定理只相对于这些公理的可靠性有效。

信任🔗

如果相信形式化定理陈述符合其预期的非形式含义，并相信导入库的作者是诚实的，则此检查有意义。

防护🔗

操作说明🔗

使用 lake build 构建项目，在包含目标定理的模块上运行 lean4checker --fresh，并确认没有报告错误。

含义🔗

lean4checker 工具读取 lean 构建时存储的声明和证明（即 .olean 文件），并通过内核重放它们。 它信任 .olean 文件在结构上是正确的。

信任🔗

如果相信形式化定理陈述符合其预期的非形式含义，并相信导入库的作者不会非常狡猾地恶意行事、不会破坏用户系统，也不会利用 Lean 的可扩展性改变定理陈述的解释，则此检查有意义。

防护🔗

备注🔗

由于 lean4checker 读取 .olean 文件时不验证格式，此检查容易受到攻击者制作无效 .olean 文件的影响（例如无效指针、字符串中的无效数据）。 Lean 策略和其他元代码运行时可以执行任意操作。 导入由决意实施恶意行为的攻击者创建的库，并在没有进一步保护的情况下构建它们，可能危及用户系统；此后就不再有有意义的检查可做。 我们建议在 CI 中运行 lean4checker，以额外防范 Lean 处理声明时的缺陷，并遏制简单攻击。 lean-action GitHub Action 可通过设置 lean4checker: true 提供此功能。

不使用 --fresh 标志时，可以让工具只检查部分模块，并假定其他模块正确（例如受信任的库），以加快处理。

操作说明🔗

在受信任环境中写下定理陈述（即“挑战”），然后按其文档启用外部检查器，将挑战和拟议证明一并交给 comparator 工具。

含义🔗

Comparator 会在沙箱环境中构建证明，以防范构建步骤中的恶意代码。 证明项会导出为序列化格式。 在沙箱外、远离可能的恶意代码时，它验证导出格式，使用 Lean 内核和/或外部检查器重放证明，并确保已证明的定理陈述与受信任挑战文件中的陈述一致。

信任🔗

如果受信任挑战文件中的定理陈述正确，且用于构建可能恶意代码的沙箱安全，则此检查有意义。

防护🔗

备注🔗

在本文撰写时，comparator 支持使用官方 Lean 内核和独立开发、以 Rust 实现的外部检查器 nanoda。Lean Kernel Arena 提供更多外部检查器，可手动使用以获得更高信心。