Trust
Axioms come from the Lean kernel (Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release)): the constants each declaration depends on, as Lean's collectAxioms reports them. Standard axioms are propext, Classical.choice and Quot.sound.
- no axioms
- 98
- standard axioms
- 182
- sorry
- 0
- extra axioms
- 0
- unknown
- 0
What the badges mean
- no axioms
- Lean's kernel checked the proof, and it rests on nothing but Lean's rules.
- standard axioms
- Checked by the kernel, using only propext, Classical.choice or Quot.sound: the three axioms nearly all of mathematics in Lean uses.
- extra axioms
- Checked by the kernel, but it assumes something the project declared with `axiom`. It is only as true as those assumptions.
- depends on sorry
- Not proved: somewhere in it, or in something it uses, a proof was left out (`sorry`).
- trust unknown
- Lean did not check it: Lean was not run, the file did not elaborate, or Lean has no constant by that name.