Satoshi's Razor

1. proposal An open problem, stated in plain language. Costless to post and carrying no formal weight: it records the idea, and who had it first.
2. sealed reading Someone translates the proposal into Lean but files only a hash of their wording - a seal - and reveals the Lean later. The hash proves the reading existed before anyone else's was public. Sealing is optional; what it buys is that independence between two readings becomes provable instead of claimed.
3. candidate statement · gloss The Lean wording goes on the log together with its gloss: the author's own plain-language reading of what their Lean actually says. No machine can check that a Lean statement means what an English sentence means, so the gloss is a claim to compare, never a certificate.
4. sorry One exact statement is pinned for solving: the Lean a solution must prove, character for character, and the environment it is checked in (core Lean, or Mathlib). The name is Lean's own - sorry is the placeholder a Lean file uses where a proof should be but nobody has written one. A sorry on this site is one of those, made public, attributed, and claimable.
5. admitted proof A submitted proof is checked automatically: it must prove exactly the pinned statement, contain no sorry inside, and rely on no unapproved axioms. A submission that passes is admitted - the checker's word for accepted, used everywhere on this site. A failing check is recorded as a rejection. Nobody rules; the kernel checks.

One kernel check shows up under three words, one per thing it settles: the submission that passed is admitted, the sorry it proved becomes solved, and a clump containing a solved statement is proven - proving one member proves them all.

Everything else on this site is a record that attaches to some point on this path. None of those records closes anything or overrules anyone - each is a signed, permanent note that readers weigh.

The same machinery has a second life for programs: in the forge, a challenge pins a formal specification, a submitted implementation is admitted only with a kernel-checked proof that it computes what the specification says (that proof obligation is an ordinary sorry), and admitted implementations then compete on measured speed. The goal is to make "fast" and "proven correct" describe the same programs. The forge's own vocabulary - rigs, lanes, boards, crowns - is explained on its page.

The registry does not start from zero and does not duplicate work that is already machine-checked elsewhere. A recognized corpus is an external body of verified work, recorded on the log with sourced statistics. Its contents count as solved: a sorry whose statement turns out to already exist in a corpus is closed by citing it, not by proving it again. New sorries should state what the corpora do not yet contain - that boundary is the frontier.

Translation into Lean can go wrong, and no machine can catch it: a statement can say less than its author meant, more, or something subtly different. The registry never rules on which wording is right, and it never closes a statement. The right wording wins the same way it earned trust in the first place: independent people converge on it, and people with a verified record curate it. Work, attention, and money follow those weights.

When a better wording exists, anyone may file a supersession mark: a public, attributed note that one sorry is better stated by another, with the reason. Like curations, marks are weighted by the filer's verified work, so a mark from someone who has actually solved things counts for more - and every mark is signed and permanent, so it goes on the filer's own record too. A mark changes no status. The marked sorry stays exactly as provable as before, its admitted proofs and payouts stand, and anyone who disagrees can keep working on it or file a mark pointing elsewhere.

What changes is what readers see: on the frontier, a marked sorry's card shows who considers it superseded and by what, sorts down in proportion to the weight against it, and links forward. A sorry's lineage number counts the earlier wordings whose marks point at it - lineage 2 means the third attempt at stating the same problem. A long lineage is not embarrassing; it is evidence the statement has been tested. Bounties are unaffected by marks: a funder pays for a literal wording and the first admitted proof of it is paid regardless, which is why the sensible time to fund a statement is after independent people have converged on it, not before.

The registry's primary rewards are the ones an append-only verified log is naturally good at: permanent attribution, timestamped priority, and standing - the same things that motivate Mathlib contributions and benchmark leaderboards today. Curation is how the community assigns importance without money: costless to file, weighted by the curator's verified work, and publicly scoreable in hindsight.

On top of that, anyone who concretely values a proof of one exact statement can attach a bounty in credits, a hypothetical accounting unit - the registry keeps the ledger and moves no real money. This layer is experimental and so far lightly used; the mechanism below is how it works, not a claim that money is flowing. Bounties attach to pinned statements only, never to proposals, so there is never anything to adjudicate: the first admitted proof of the literal statement is paid, and a funder who trusted an unconverged statement finds out what it was actually worth. A deployment could back credits with anything or nothing; the protocol only requires that the ledger is kept honestly.

The mechanisms above are easiest to see in motion. What follows is the demo dataset's walkthrough: the participants are fictional, but every proof check and every event is really produced by running the system. One sorting problem is formalized too weakly, funded too early, and goes through the whole process. When the demo dataset is loaded, each step cites the log events it produced.