A compass in the formalization of all indexed and published mathematics.
Correctness profile — how each statement stands against formal verification
a paper marked detected has a known formalization artifact (e.g. a mathlib declaration) that has not yet been assessed into the profile above — formalization is confirmed to exist; how much is not yet quantified.