Trust

Axioms come from the Lean kernel (Lean (version 4.34.1, x86_64-w64-windows-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release)): the constants each declaration depends on, as Lean's collectAxioms reports them. Standard axioms are propext, Classical.choice and Quot.sound.

Lake environment and dependency-pin digest: c34b4267063e8a41.

Verification scope: upstream formalization.yaml main-result catalogue; 192 of 192 eligible files selected, 200 declarations requested.

Rendering mode: clean content-bound cache results only; 167 selected files had no reusable result and remain UNKNOWN. No Lean process was started for those misses during this static-site build.

Per-file probe bounds: 300 seconds, 5120 MiB maximum working set, stop below 10240 MiB free virtual memory. A resource stop is UNKNOWN, never a failed proof.

no axioms
0
standard axioms
26
sorry
0
extra axioms
0
unknown
3566237

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.

Files outside this Lean pass (122391)