Every precisely stated open problem in the registry, together with the ones already solved: what each sorry asks, the exact Lean statement a solution must prove, and what it would take to close it.
Each card shows any bounty attached to the exact statement, who has curated it and why, every attempt with the checker's verdict, and the full event history. The attention sort is one estimate of how much a sorry currently matters: bounty credits at face value, plus fixed weights for each community signal - 900 per clump-weight point (people independently writing equivalent statements), 800 per equivalence proof, 700 per curation-weight point (curations count more from people with accepted proofs), 600 per earlier wording replaced, 500 per registered split, and 250 per attempt - plus 400 while it is open, minus 700 per supersession-mark weight point (attributed notes that a better wording exists). The weights are convention, not judgment: every input is listed on the sorry's own page, and hovering any badge explains it.
A proposal is a problem in plain language. Anyone may attach a candidate statement: a Lean formalization together with its author's own plain-language reading (the gloss). Statements proven equivalent to each other form a clump; a clump's weight counts its distinct authors, because two people independently writing equivalent formalizations is the strongest available evidence that both mean what the proposal means. The unique heaviest clump with at least two independent members is dominant - the reading the community has converged on, and the signal a funder should wait for before putting a bounty on any statement.
The labels on a clump are computed from the log, not decided by anyone: proven means some member statement has an admitted proof (proving one member proves them all, since they are equivalent). A statement that is proven, has one author, and took milliseconds to check is usually a mistranslation that says less than intended - but that is for the reader to conclude; no label here says it.
Proposals ingested from sourced catalogues (the 1000+ theorems list) that no one
has formalized yet: a to-do list for formalized mathematics. Each needs a pinned statement in the
Mathlib environment before it is a solvable sorry - filing that statement is itself attributed,
timestamped work on the log. To claim one: open it, read the background, then
razor formalize --gloss "your plain-language reading". A problem missing from the
list can be proposed straight from the browser - no Lean, no account.