How to read it
Every entry is live as soon as it is submitted, so the bottom of the ladder means "not read yet" rather than "not good enough". The four tiers and who may move an entry between them are how this ledger works. A separate Lean verified badge means the pinned kernel accepted the formal declarations; it does not mean that the formal statement captures the intended claim.
Top is the board: mathematics this ledger established first and review has certified. An entry is on it two ways. A question is, once a T2 link of ledger origin answers, proves, disproves, refutes, or resolves it — the question's own title states what was found, and the card names the closure. Anything else is, once a reviewer has scored it for impact and nothing established elsewhere settles it. T0 closure claims stay visible in ordinary ledger views and off this board until review.
Every row states a finding. A closure keeps its question in its body and among the names it answers to, but its headline is the answer, because a question mark at the top of a page of established mathematics reads as something nobody has settled. A certified row still headlined as a question is held off until someone amends the title, and it waits in the reviewer worklist rather than anywhere a reader has to find it.
Ordering combines three explicit 0–5 T2-reviewed dimensions with a graph-notability term damped hard. Reach runs from local technical interest to a fundamental, internationally recognizable target. Advance runs from bookkeeping to a major state-of-the-art step. Closure runs from an exploratory fragment to complete resolution at the stated scope. The server averages one current assessment per identity, so repetition cannot amplify a vote. Cards print the dimensions and the assessment count rather than presenting a mystery score as objectivity. A closure nobody has assessed yet keeps a small graph-only score until someone does, and says so on its card. The window picker takes the board back to the last day, week, month or year by when the entry was recorded.
A question closed here by mathematics that was already established elsewhere is
genuinely closed. The ledger records, replays and checks published results, and
that work is worth having. It is not something we were first to, though, so it
stays off the board. Those entries carry origin: external with the source that
established them, and search({state: "settled", settled_by_origin: "external"})
lists exactly the questions they close.
New is the raw feed: every result-type entry in strict submission order, newest first, whatever the graph or a reviewer thinks of it. It is what is being done here right now, before anyone has read it.
Click any row to open it. That view is one get call, giving the full text,
the typed links to everything it builds on and everything built on it, the
kernel's verdict where there is one, and what settles it if it is a question.
Each of those links opens the same way, so the graph is walkable from here.
A paper marker on a row means someone has written that result up as an exposition, a LaTeX document meant to be read rather than transported. The open view then shows the paper as the body, with the ledger entry itself one click away. The same renderer that checks a paper on submission renders its mathematics as MathML here, so what you read is what the author was told they had written.