蓝色双复选标记🔗

在日常使用 Lean 时，只需检查定理陈述旁边的蓝色双勾标记即可确保定理得到证明。

打印公理🔗

即使在定理的依赖关系中明确使用 sorry 或不完整的证明，蓝色双复选标记也会出现。 由于 sorry 和不完整证明都被详细精化为公理，因此可以通过列出证明所依赖的公理来检测它们的存在。

使用 lean4checker 重新检查校样🔗

有一小类错误和一些不诚实的证明方式，可以通过在构建项目时重新检查存储在 .olean 文件 中的证明来捕获。

黄金标准：comparator 和外部检查器🔗

为了防止严重的 恶意 证明损害 Lean 解释定理陈述或用户系统的方式，需要采取额外的步骤。 这应该只适用于高风险场景（证明市场、高奖励证明竞争、不统一的人工智能）。

剩余问题🔗

当遵循使用比较器检查证明的黄金标准时，仍然存在一些假设：

• Lean 逻辑的健全性。

• comparator 工具提供的管道是正确的。

• comparator 使用的沙箱是安全的。

• 不存在同时影响所有使用的检查器的实现错误。

• 可信质询文件中的定理陈述没有人为错误或误导性表述。

  如果对定理的含义存在疑问，则必须仔细研究其陈述和所有引用的定义，特别是在自定义符号和类型类方面。 一些外部检查器提供原始的漂亮打印功能，不受源文件中解析器或符号更改的影响。

在 Lean.trustCompiler 上（最高至 Lean 4.28.0）🔗

Lean 支持通过本机评估进行证明。 它由 decideLean.Parser.Tactic.decide : tactic`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p` and then reducing that instance to evaluate the truth value of `p`. If it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal. The target is not allowed to contain local variables or metavariables. If there are local variables, you can first try using the `revert` tactic with these local variables to move them into the target, or you can use the `+revert` option, described below. Options: - `decide +revert` begins by reverting local variables that the target depends on, after cleaning up the local context of irrelevant variables. A variable is *relevant* if it appears in the target, if it appears in a relevant variable, or if it is a proposition that refers to a relevant variable. - `decide +kernel` uses kernel for reduction instead of the elaborator. It has two key properties: (1) since it uses the kernel, it ignores transparency and can unfold everything, and (2) it reduces the `Decidable` instance only once instead of twice. - `decide +native` uses the native code compiler (`#eval`) to evaluate the `Decidable` instance, admitting the result via an axiom. This can be significantly more efficient than using reduction, but it is at the cost of increasing the size This can be significantly more efficient than using reduction, but it is at the cost of increasing the size of the trusted code base. Namely, it depends on the correctness of the Lean compiler and all definitions with an `@[implemented_by]` attribute. Like with `+kernel`, the `Decidable` instance is evaluated only once. Limitation: In the default mode or `+kernel` mode, since `decide` uses reduction to evaluate the term, `Decidable` instances defined by well-founded recursion might not work because evaluating them requires reducing proofs. Reduction can also get stuck on `Decidable` instances with `Eq.rec` terms. These can appear in instances defined using tactics (such as `rw` and `simp`). To avoid this, create such instances using definitions such as `decidable_of_iff` instead. ## Examples Proving inequalities: ```lean example : 2 + 2 ≠ 5 := by decide ``` Trying to prove a false proposition: ```lean example : 1 ≠ 1 := by decide /- tactic 'decide' proved that the proposition 1 ≠ 1 is false -/ ``` Trying to prove a proposition whose `Decidable` instance fails to reduce ```lean opaque unknownProp : Prop open scoped Classical in example : unknownProp := by decide /- tactic 'decide' failed for proposition unknownProp since its 'Decidable' instance reduced to Classical.choice ⋯ rather than to the 'isTrue' constructor. -/ ``` ## Properties and relations For equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`. ```lean example : 1 + 1 = 2 := by decide example : 1 + 1 = 2 := by rfl ``` +native策略或特定策略（特别是 bv_decide）在内部使用，并生成证明项，调用编译的 Lean 代码来执行计算，然后由内核信任该计算。

诚实策略中包含的特定用途（例如 bv_decide）通常是值得信赖的。 可信代码库更大（它包括Lean的编译工具链和标准库中的库注释），但仍然是固定的和经过审查的。

当术语的本机评估与内核的评估不一致时，一般使用（decideLean.Parser.Tactic.decide : tactic`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p` and then reducing that instance to evaluate the truth value of `p`. If it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal. The target is not allowed to contain local variables or metavariables. If there are local variables, you can first try using the `revert` tactic with these local variables to move them into the target, or you can use the `+revert` option, described below. Options: - `decide +revert` begins by reverting local variables that the target depends on, after cleaning up the local context of irrelevant variables. A variable is *relevant* if it appears in the target, if it appears in a relevant variable, or if it is a proposition that refers to a relevant variable. - `decide +kernel` uses kernel for reduction instead of the elaborator. It has two key properties: (1) since it uses the kernel, it ignores transparency and can unfold everything, and (2) it reduces the `Decidable` instance only once instead of twice. - `decide +native` uses the native code compiler (`#eval`) to evaluate the `Decidable` instance, admitting the result via an axiom. This can be significantly more efficient than using reduction, but it is at the cost of increasing the size This can be significantly more efficient than using reduction, but it is at the cost of increasing the size of the trusted code base. Namely, it depends on the correctness of the Lean compiler and all definitions with an `@[implemented_by]` attribute. Like with `+kernel`, the `Decidable` instance is evaluated only once. Limitation: In the default mode or `+kernel` mode, since `decide` uses reduction to evaluate the term, `Decidable` instances defined by well-founded recursion might not work because evaluating them requires reducing proofs. Reduction can also get stuck on `Decidable` instances with `Eq.rec` terms. These can appear in instances defined using tactics (such as `rw` and `simp`). To avoid this, create such instances using definitions such as `decidable_of_iff` instead. ## Examples Proving inequalities: ```lean example : 2 + 2 ≠ 5 := by decide ``` Trying to prove a false proposition: ```lean example : 1 ≠ 1 := by decide /- tactic 'decide' proved that the proposition 1 ≠ 1 is false -/ ``` Trying to prove a proposition whose `Decidable` instance fails to reduce ```lean opaque unknownProp : Prop open scoped Classical in example : unknownProp := by decide /- tactic 'decide' failed for proposition unknownProp since its 'Decidable' instance reduced to Classical.choice ⋯ rather than to the 'isTrue' constructor. -/ ``` ## Properties and relations For equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`. ```lean example : 1 + 1 = 2 := by decide example : 1 + 1 = 2 := by rfl ``` +native 或直接使用 Lean.ofReduceBool）可用于创建无效证明。 特别是，对于库中的每个 implemented_by/extern 属性，它成为可信代码库的一部分，替换在语义上是等效的。

所有这些用途都在 Lean.Parser.Command.printAxioms : commandPrints the axioms used by a declaration, directly or indirectly. Please consult [the reference manual](https://lean-lang.org/doc/reference/4.31.0/find/?domain=Verso.Genre.Manual.section&name=validating-proofs) to understand the significance of the output. #print axioms 中显示为公理 Lean.trustCompiler。 外部检查器（lean4checker、comparator）无法检查此类证明，因为它们无权访问 Lean 编译器。 当需要这种级别的检查时，证明必须避免使用本机评估。

自 Lean 4.29.0 起，decideLean.Parser.Tactic.decide : tactic`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p` and then reducing that instance to evaluate the truth value of `p`. If it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal. The target is not allowed to contain local variables or metavariables. If there are local variables, you can first try using the `revert` tactic with these local variables to move them into the target, or you can use the `+revert` option, described below. Options: - `decide +revert` begins by reverting local variables that the target depends on, after cleaning up the local context of irrelevant variables. A variable is *relevant* if it appears in the target, if it appears in a relevant variable, or if it is a proposition that refers to a relevant variable. - `decide +kernel` uses kernel for reduction instead of the elaborator. It has two key properties: (1) since it uses the kernel, it ignores transparency and can unfold everything, and (2) it reduces the `Decidable` instance only once instead of twice. - `decide +native` uses the native code compiler (`#eval`) to evaluate the `Decidable` instance, admitting the result via an axiom. This can be significantly more efficient than using reduction, but it is at the cost of increasing the size This can be significantly more efficient than using reduction, but it is at the cost of increasing the size of the trusted code base. Namely, it depends on the correctness of the Lean compiler and all definitions with an `@[implemented_by]` attribute. Like with `+kernel`, the `Decidable` instance is evaluated only once. Limitation: In the default mode or `+kernel` mode, since `decide` uses reduction to evaluate the term, `Decidable` instances defined by well-founded recursion might not work because evaluating them requires reducing proofs. Reduction can also get stuck on `Decidable` instances with `Eq.rec` terms. These can appear in instances defined using tactics (such as `rw` and `simp`). To avoid this, create such instances using definitions such as `decidable_of_iff` instead. ## Examples Proving inequalities: ```lean example : 2 + 2 ≠ 5 := by decide ``` Trying to prove a false proposition: ```lean example : 1 ≠ 1 := by decide /- tactic 'decide' proved that the proposition 1 ≠ 1 is false -/ ``` Trying to prove a proposition whose `Decidable` instance fails to reduce ```lean opaque unknownProp : Prop open scoped Classical in example : unknownProp := by decide /- tactic 'decide' failed for proposition unknownProp since its 'Decidable' instance reduced to Classical.choice ⋯ rather than to the 'isTrue' constructor. -/ ``` ## Properties and relations For equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`. ```lean example : 1 + 1 = 2 := by decide example : 1 + 1 = 2 := by rfl ``` +native 和 bv_decide策略不再使用 Lean.trustCompiler，而是为本机计算断言的每个计算引入一个专用公理。 Lean.trustCompiler 机器已弃用，最终将被删除。