公理可能单独或与其他公理结合引入不一致。

假设一个错误的陈述允许任何陈述被证明：

axiom false_is_true : False theorem two_eq_five : 2 = 5 := false_is_true.elim

与 Lean 的其他属性不兼容的公理也可能引起不一致。 例如，参数性在支持它的语言中使用时是一种强大的推理技术，但它与 Lean 的标准公理不兼容。 如果参数性成立，那么 Wadler 的 Theorems for Free (1989) 介绍中的“自由定理”将是正确的，该定理描述了一种使用参数性推导有关多态函数的定理的技术。 作为一条公理，它写道：

axiom List.free_theorem {α β} (f : {α : _} → List α → List α) (g : α → β) : f ∘ (List.map g) = (List.map g) ∘ f

然而，排中的结果是所有命题都是可判定的；这意味着函数可以检查它们是真还是假。 这个函数无法编译，但它仍然存在。 这可用于定义非参数的多态函数：

open Classical in noncomputable def nonParametric {α : _} (xs : List α) : List α := if α = Nat then [] else xs

这个函数的存在与“自由定理”相矛盾：

theorem unit_not_nat : Unit ≠ Nat := by⊢ Unit ≠ Nat intro eqeq:Unit = Nat⊢ False have ⟨allEq⟩ := eq ▸ (inferInstance : Subsingleton Unit)eq:Unit = NatallEq:∀ (a b : Nat), a = b⊢ False specialize allEq 0 1eq:Unit = NatallEq:0 = 1⊢ False contradictionAll goals completed! 🐙 example : False := by⊢ False have := List.free_theorem nonParametric (fun () => 42)this:(nonParametric ∘ List.map fun x => 42) = (List.map fun x => 42) ∘ nonParametric⊢ False unfold nonParametric at thisthis:((fun xs => if Nat = Nat then [] else xs) ∘ List.map fun x => 42) = (List.map fun x => 42) ∘ fun xs => if Unit = Nat then [] else xs⊢ False simp [unit_not_nat] at thisthis:((fun xs => []) ∘ List.map fun x => 42) = (List.map fun x => 42) ∘ fun xs => xs⊢ False have := congrFun this [()]this✝:((fun xs => []) ∘ List.map fun x => 42) = (List.map fun x => 42) ∘ fun xs => xsthis:((fun xs => []) ∘ List.map fun x => 42) [()] = ((List.map fun x => 42) ∘ fun xs => xs) [()]⊢ False contradictionAll goals completed! 🐙

使用公理向 Nat 添加额外的 0 会导致一些定义归约陷入困境。 在此示例中，两个 Nat.succ 构造函数通过归约成功移至项外，但 Nat.rec 在遇到 Nat.otherZero 后无法取得进一步的进展。

axiom Nat.otherZero : Nat ((Nat.rec ⟨fun x => x, PUnit.unit⟩ (fun n n_ih => ⟨fun x => (n_ih.1 x).succ, n_ih⟩) Nat.otherZero).1 4).succ.succ#reduce 4 + (Nat.otherZero + 2)

((Nat.rec ⟨fun x => x, PUnit.unit⟩ (fun n n_ih => ⟨fun x => (n_ih.1 x).succ, n_ih⟩) Nat.otherZero).1 4).succ.succ

使用公理向 Nat 添加额外的 0 会使使用它的函数无法编译。 特别是，List.length' 返回公理 Nat.otherZero 而不是 Nat.zero 作为空列表的长度。

axiom Nat.otherZero : Nat def `Nat.otherZero` not supported by code generator; consider marking definition as `noncomputable`List.length' : List α → Nat | [] => Nat.otherZero | _ :: _ => Unknown identifier `xs.length`xs.length

`Nat.otherZero` not supported by code generator; consider marking definition as `noncomputable`

在证明中而不是在程序中使用的公理不会阻止函数的编译。 编译器不会生成证明代码，因此证明中的公理没有问题。 nextOdd 从 Nat 计算下一个奇数，该奇数可以是数字本身或更大的数字：

def nextOdd (k : Nat) : { n : Nat // n % 2 = 1 ∧ (n = k ∨ n = k + 1) } where val := if k % 2 = 1 then k else k + 1 property := byk:Nat⊢ (if k % 2 = 1 then k else k + 1) % 2 = 1 ∧ ((if k % 2 = 1 then k else k + 1) = k ∨ (if k % 2 = 1 then k else k + 1) = k + 1) by_cases k % 2 = 1posk:Nath✝:k % 2 = 1⊢ (if k % 2 = 1 then k else k + 1) % 2 = 1 ∧ ((if k % 2 = 1 then k else k + 1) = k ∨ (if k % 2 = 1 then k else k + 1) = k + 1)negk:Nath✝:¬k % 2 = 1⊢ (if k % 2 = 1 then k else k + 1) % 2 = 1 ∧ ((if k % 2 = 1 then k else k + 1) = k ∨ (if k % 2 = 1 then k else k + 1) = k + 1) <;>posk:Nath✝:k % 2 = 1⊢ (if k % 2 = 1 then k else k + 1) % 2 = 1 ∧ ((if k % 2 = 1 then k else k + 1) = k ∨ (if k % 2 = 1 then k else k + 1) = k + 1)negk:Nath✝:¬k % 2 = 1⊢ (if k % 2 = 1 then k else k + 1) % 2 = 1 ∧ ((if k % 2 = 1 then k else k + 1) = k ∨ (if k % 2 = 1 then k else k + 1) = k + 1) simp [*]negk:Nath✝:¬k % 2 = 1⊢ (k + 1) % 2 = 1 <;>negk:Nath✝:¬k % 2 = 1⊢ (k + 1) % 2 = 1 omegaAll goals completed! 🐙

策略证明生成一个传递依赖于三个公理的项：

'nextOdd' depends on axioms: [propext, Classical.choice, Quot.sound]#print axioms nextOdd

'nextOdd' depends on axioms: [propext, Classical.choice, Quot.sound]

因为它们只出现在证明中，所以编译器生成代码没有问题：

(5, 5)#eval (nextOdd 4, nextOdd 5)

(5, 5)

The functions Lean.reduceBool and Lean.reduceNat can be invoked to have the compiler perform a calculation; this can greatly improve performance of implementations of proof by reflection.

def largeNumber : Nat := `Lean.reduceNat` has been deprecated: in-kernel native reduction is deprecated; assert native evaluations with axioms insteadLean.reduceNat (230_000 + 4_500 + 1_000_067)

The resulting term depends on the axiom Lean.trustCompiler in order to track the fact that this calculation depends on the correctness of the compiler.

'largeNumber' depends on axioms: [Lean.trustCompiler]#print axioms largeNumber

'largeNumber' depends on axioms: [Lean.trustCompiler]

Instead of appealing to Lean.trustCompiler, the native_decide tactic creates a bespoke axiom for each invocation. This allows each axiom to be audited for the precise statement that it proves.

def bigSum : (List.range 1_001).sum = 500_500 := by⊢ (List.range 1001).sum = 500500 native_decideAll goals completed! 🐙 'bigSum' depends on axioms: [bigSum._native.native_decide.ax_1]#print axioms bigSum

'bigSum' depends on axioms: [bigSum._native.native_decide.ax_1]

The axiom's type can be checked directly:

bigSum._native.native_decide.ax_1 : decide ((List.range 1001).sum = 500500) = true#check bigSum._native.native_decide.ax_1

bigSum._native.native_decide.ax_1 : decide ((List.range 1001).sum = 500500) = true

Consider the following three constants:

def addThree (n : Nat) : Nat := 1 + n + 2 theorem excluded_middle (P : Prop) : P ∨ ¬ P := Classical.em P theorem simple_equality (P : Prop) : (P ∨ False) = P := or_false P

Regular functions like addThree that we might want to actually evaluation typically do not depend on any axioms:

'addThree' does not depend on any axioms#print axioms addThree

'addThree' does not depend on any axioms

The excluded middle theorem is only true if we use classical reasoning, so the foundation for classical reasoning shows up alongside other axioms:

'excluded_middle' depends on axioms: [propext, Classical.choice, Quot.sound]#print axioms excluded_middle

'excluded_middle' depends on axioms: [propext, Classical.choice, Quot.sound]

Finally, the idea that two equivalent propositions are equal directly relies on propositional extensionality.

'simple_equality' depends on axioms: [propext]#print axioms simple_equality

'simple_equality' depends on axioms: [propext]

You can use 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 together with Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd` and checks that they match the contents of the docstring. Basic example: ```lean /-- error: Unknown identifier `x` -/ #guard_msgs in example : α := x ``` This checks that there is such an error and then consumes the message. By default, the command captures all messages, but the filter condition can be adjusted. For example, we can select only warnings: ```lean /-- warning: declaration uses 'sorry' -/ #guard_msgs(warning) in example : α := sorry ``` or only errors ```lean #guard_msgs(error) in example : α := sorry ``` In the previous example, since warnings are not captured there is a warning on `sorry`. We can drop the warning completely with ```lean #guard_msgs(error, drop warning) in example : α := sorry ``` In general, `#guard_msgs` accepts a comma-separated list of configuration clauses in parentheses: ``` #guard_msgs (configElt,*) in cmd ``` By default, the configuration list is `(check all, whitespace := normalized, ordering := exact, positions := false)`. Message filters select messages by severity: - `info`, `warning`, `error`: (non-trace) messages with the given severity level. - `trace`: trace messages - `all`: all messages. The filters can be prefixed with the action to take: - `check` (the default): capture and check the message - `drop`: drop the message - `pass`: let the message pass through If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in left-to-right order, with an implicit `pass all` at the end. Whitespace handling (after trimming leading and trailing whitespace): - `whitespace := exact` requires an exact whitespace match. - `whitespace := normalized` converts all newline characters to a space before matching (the default). This allows breaking long lines. - `whitespace := lax` collapses whitespace to a single space before matching. Message ordering: - `ordering := exact` uses the exact ordering of the messages (the default). - `ordering := sorted` sorts the messages in lexicographic order. This helps with testing commands that are non-deterministic in their ordering. Position reporting: - `positions := true` reports the ranges of all messages relative to the line on which `#guard_msgs` appears. - `positions := false` does not report position info. Substring matching: - `substring := true` checks that the docstring appears as a substring of the output (after whitespace normalization). This is useful when you only care about part of the message. - `substring := false` (the default) requires exact matching (modulo whitespace normalization). Stabilizing output: When messages contain autogenerated names (e.g., metavariables like `?m.47`), the output may differ between runs or Lean versions. Use `set_option pp.mvars.anonymous false` to replace anonymous metavariables with `?_` while preserving user-named metavariables like `?a`. Alternatively, `set_option pp.mvars false` replaces all metavariables with `?_`. Similarly, `set_option pp.fvars.anonymous false` replaces loose free variable names like `_fvar.22` with `_fvar._`. For example, `#guard_msgs (error, drop all) in cmd` means to check errors and drop everything else. The command elaborator has special support for `#guard_msgs` for linting. The `#guard_msgs` itself wants to capture linter warnings, so it elaborates the command it is attached to as if it were a top-level command. However, the command elaborator runs linters for *all* top-level commands, which would include `#guard_msgs` itself, and would cause duplicate and/or uncaptured linter warnings. The top-level command elaborator only runs the linters if `#guard_msgs` is not present. #guard_msgs to ensure that updates to libraries from other projects cannot silently introduce unwanted dependencies on axioms.

For example, if the proof of double_neg_elim below changed in such a way that it used more axioms than those listed, then the Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd` and checks that they match the contents of the docstring. Basic example: ```lean /-- error: Unknown identifier `x` -/ #guard_msgs in example : α := x ``` This checks that there is such an error and then consumes the message. By default, the command captures all messages, but the filter condition can be adjusted. For example, we can select only warnings: ```lean /-- warning: declaration uses 'sorry' -/ #guard_msgs(warning) in example : α := sorry ``` or only errors ```lean #guard_msgs(error) in example : α := sorry ``` In the previous example, since warnings are not captured there is a warning on `sorry`. We can drop the warning completely with ```lean #guard_msgs(error, drop warning) in example : α := sorry ``` In general, `#guard_msgs` accepts a comma-separated list of configuration clauses in parentheses: ``` #guard_msgs (configElt,*) in cmd ``` By default, the configuration list is `(check all, whitespace := normalized, ordering := exact, positions := false)`. Message filters select messages by severity: - `info`, `warning`, `error`: (non-trace) messages with the given severity level. - `trace`: trace messages - `all`: all messages. The filters can be prefixed with the action to take: - `check` (the default): capture and check the message - `drop`: drop the message - `pass`: let the message pass through If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in left-to-right order, with an implicit `pass all` at the end. Whitespace handling (after trimming leading and trailing whitespace): - `whitespace := exact` requires an exact whitespace match. - `whitespace := normalized` converts all newline characters to a space before matching (the default). This allows breaking long lines. - `whitespace := lax` collapses whitespace to a single space before matching. Message ordering: - `ordering := exact` uses the exact ordering of the messages (the default). - `ordering := sorted` sorts the messages in lexicographic order. This helps with testing commands that are non-deterministic in their ordering. Position reporting: - `positions := true` reports the ranges of all messages relative to the line on which `#guard_msgs` appears. - `positions := false` does not report position info. Substring matching: - `substring := true` checks that the docstring appears as a substring of the output (after whitespace normalization). This is useful when you only care about part of the message. - `substring := false` (the default) requires exact matching (modulo whitespace normalization). Stabilizing output: When messages contain autogenerated names (e.g., metavariables like `?m.47`), the output may differ between runs or Lean versions. Use `set_option pp.mvars.anonymous false` to replace anonymous metavariables with `?_` while preserving user-named metavariables like `?a`. Alternatively, `set_option pp.mvars false` replaces all metavariables with `?_`. Similarly, `set_option pp.fvars.anonymous false` replaces loose free variable names like `_fvar.22` with `_fvar._`. For example, `#guard_msgs (error, drop all) in cmd` means to check errors and drop everything else. The command elaborator has special support for `#guard_msgs` for linting. The `#guard_msgs` itself wants to capture linter warnings, so it elaborates the command it is attached to as if it were a top-level command. However, the command elaborator runs linters for *all* top-level commands, which would include `#guard_msgs` itself, and would cause duplicate and/or uncaptured linter warnings. The top-level command elaborator only runs the linters if `#guard_msgs` is not present. #guard_msgs command would report an error.

theorem double_neg_elim (P : Prop) : (¬ ¬ P) = P := propext Classical.not_not /-- info: 'double_neg_elim' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms double_neg_elim