VibeRegistry — statement search
Lean statements this registry has checked, plus mirrored entries
from upstream registries. A machine check says the proof establishes the
statement; a sign-off says a human read the statement.
Anyone can sign off: pick a statement below and use its link, or
open a blank sign-off .
What a sign-off means and how to prepare one .
Loading…
What a row means. A machine check says an implementation
proves the statement. A sign-off says a named human read the statement and
vouched for what it says. They are different claims, and a row shows both or
neither — an unsigned statement is listed, not hidden.
Mirrored rows come from Palomar
and LeanPool , which checked
them; this registry did not re-verify those proofs.
Source and
documentation ·
Submit a sign-off ·
How sign-off works ·
raw index