WP-75 states it once and everything follows:
An outcome can be paid for on verifiable terms if and only if its before-state is observable and dated in an archive that neither party controls.
Avoided deforestation fails it: the before-state is a forest that still stands and the claim concerns a future that did not occur. Restoration of degraded ground passes: bare ground is spectrally unambiguous and the public satellite archive holds a dated record predating any contract.
Apply it to a mathematical obligation. DERIVED
| Clause | Land (WP-75’s best case) | A formal obligation |
|---|---|---|
| before-state observable | bare ground, spectrally | sorry stands in the source text |
| dated | scene ID and acquisition date | the commit that wrote it |
| archive neither party controls | public satellite archive — yes | partial — §5 |
| after-state checkable by a third party | canopy, over years | one gate run, seconds |
| forgeable by the claimant | baselines are chosen by the paid party | no — the kernel does not take a word |
Four of five clauses pass more cleanly here than in the domain WP-75 was written for. The fifth is the whole of §5.
WP-75’s binding constraint was detection asymmetry, and it ran the wrong way for the thing worth paying for. Clearing is loud — abrupt, high-contrast, mapped in near-real time. Establishment is quiet — a planted seedling is sub-pixel and spectrally indistinguishable for years. The destructive act is easy to see; the constructive one is not, and that is why the payment had to be staged against canopy years later and pinned to immutable scene IDs.
Closing an obligation is loud. The gate report changes; a line that read depends on axioms: [sorryAx, …] now reads without it, or the declaration moves from admitted to audited. The change is discrete, immediate, and machine-visible.
And faking it is impossible rather than merely hard, which has no analogue in land at all. A claimant cannot assert a proof into existence: the kernel elaborates the term or it does not. There is no baseline for the paid party to choose, because there is no baseline — there is a check.
That is the difference between a market that needs a registry, an auditor and a permanence buffer, and one that needs a build.
Pay per theorem and the first thing bought is this:
It compiles. It contains no sorry. It reports the standard three axioms, and is indistinguishable from a real theorem to every automated check including this repository’s. Six such statements are live in this corpus right now and are listed by name in Orthogenesis/Architecture/KNOWN_PLACEHOLDERS.txt, whose rule is the relevant governance primitive: declared-open is acceptable; undeclared-open fails the build. MEASURED
Not a theorem produced. A named obligation closed — a statement written down, in advance, by the party who wants it discharged. Vacuity becomes impossible not because it is detected but because the statement is not the claimant’s to choose. The buyer fixes the type; the seller supplies a term of it. That is the whole of the anti-gaming design and it is one sentence long. DESIGN
The corpus has the supply to demonstrate the unit is not hypothetical: 275 open obligations across 81 files, out of 2,812 tracked declarations. MEASURED Each is a statement someone wrote down and did not close. That is an inventory, not a market, and §6 is about the difference.
WP-73 enumerated the classes and, crucially, what detects each. Two of them bound this market permanently.
| Class | Priceable? | Why |
|---|---|---|
| admitted → kernel-audited | yes | machine-decidable, cheap, unforgeable |
| VACUOUS | partly | a declared baseline catches the known ones; only the elaborated type catches the rest |
| MISATTRIBUTED | no, and nothing can | whether a true statement supports the claim made from it is not mechanisable, and WP-73 says so as a finding rather than a limitation of its instrument |
So the boundary is sharp and worth stating as a warning rather than a caveat: this market can price the closure of a stated obligation. It cannot price significance, and no version of it ever will. Anyone offering to pay for important theorems on verifiable terms is selling MISATTRIBUTED, which is the class with an empty detection column. DERIVED
That is not fatal; it is a scope. Significance is priced the way it always has been — by someone deciding which obligation to post, and paying to have that one closed. The judgement stays with the buyer, where it is already, and where nothing pretends to automate it.
WP-75 §7 rejected a token design, and the rejection was not squeamishness. It rested on a completed experiment: bridging carbon credits onto public ledgers in 2021–22 concentrated demand in the oldest and lowest-quality inventory, because the bridge could not discriminate on quality, and the registry moved to block it. WP-75’s diagnosis is the sentence to carry forward:
No amount of ledger integrity repairs an unobservable measurand. An immutable record of an unverifiable claim is an unverifiable claim that can no longer be corrected.
That reason does not transfer, because here the measurand is observable — which is the entire point of §§1–2. But two of WP-75’s findings transfer intact and constrain any design:
And the clause still unmet. WP-75 requires an archive neither party controls. A git host is a party; a repository owner can rewrite history. This is the one place where the analogy to the satellite archive is currently weaker rather than stronger, and it is a solved problem in kind rather than in fact — a public deposit with a DOI, a timestamped hash in a record neither side administers. This note does not design that, endorses no instrument, proposes no token, and is not financial advice of any kind. It states the requirement and stops. OPEN
The honest answer is that this is the weakest section and the one with no evidence in it. An inventory is not demand. Three candidate buyers exist and each has a stated reason and an unstated problem.
| Buyer | Why they would | What is unknown |
|---|---|---|
| the party needing the obligation closed | an assurance case with a hole in it is worth closing; the hole is already named | whether such parties currently write their obligations formally at all — mostly they do not |
| research funders | a funded output that is machine-checkable is the only kind whose delivery is not a matter of trust; the AI Action Plan asks for exactly this discipline (WP-98 §1) | no programme prices work this way today |
| model developers | formally checked corpora carry a ground-truth signal that ordinary text does not, and the check is the label | this is the one live market of the three, and its terms are not public |
What makes the job possible rather than likely is §3 of WP-98: on a hub whose outputs are machine-checkable the credential requirement falls, because the artefact carries the argument. A person who can close a named obligation is paid for the closure, and the closure is checked by a kernel that does not know who they are. That is a labour market with an unusually low barrier and an unusually hard qualification — easy to enter, impossible to fake.
The section above looks for demand. The objection is that demand need not be found at all: Bitcoin did not discover a demand for hashing, it manufactured one. A protocol pays a reward to whoever exhibits work, and the work acquires a price because the protocol says so. If that can be done for a computation with no use whatever, it can be done for one that closes a theorem.
The instinct is right and the mechanism named is the wrong one. Proof-of-work and proof-of-theorem share the asymmetry — expensive to produce, cheap to check, impossible to fake — and that resemblance is why the analogy is tempting. Three properties that mining requires are absent here, and each absence is structural rather than an engineering gap. DERIVED
| Mining requires | Formal obligations |
|---|---|
| a difficulty dial. Block time is held constant by making the puzzle harder or easier on a schedule | there is no dial. You cannot make a conjecture three percent harder next fortnight, and an obligation’s difficulty is not known until it is closed — sometimes not until decades after it is posted |
| memorylessness. Each hash has the same chance as every other, so reward tracks expenditure and distributes | not memoryless — the chance is not proportional to expenditure and never will be. But the first draft of this row said “skill and prior work dominate completely”, which is corrected below and is wrong in the paper’s own named way |
| an inexhaustible puzzle. The next block always exists | an obligation is closed once. Each closure permanently removes one from the supply |
The middle row above first read: skill and prior work dominate completely; the reward concentrates, and concentrates on the people who least need an incentive. Mining’s property does fail here and that part stands — the chance of closing an obligation is not proportional to expenditure. What does not stand is the second half, which fixed a parameter and read it as a constant of nature: that capability in this work is a function of training history. That is OVER-GENERALISED (WP-97), and it is the third instance in this series in a week.
It also contradicts WP-98 §8, in this volume, written days earlier and by the same author. That section argues that on a hub whose outputs are machine-checkable the credential requirement falls to near zero, because the artefact carries the argument instead of the author carrying a reputation. A row asserting that prior work dominates is that argument, denied, one paper later.
Theorem-closing is not memoryless and cannot be made so. It is also not the strongly path-dependent tournament the first draft implied. The variance in who closes a given obligation is higher than a seniority model predicts, and the direction of travel is toward wider access, because the part of “prior work” that consisted of tooling fluency — knowing which lemma exists, what it is called, how the library is shaped — is exactly the part an assistant supplies.
Both the concentrating and the distributing claim are currently unmeasured. §7 of WP-98 already names the measurement: contributor pedigree over time in a corpus whose acceptance criterion is a kernel rather than a committee. Neither paper has run it. OPEN
The correction does more than repair a row. A market is worth running only when the identity of the supplier is uncertain. If you can predict who will close an obligation, you do not post a bounty — you hire that person, and the whole apparatus of §§1–5 is unnecessary overhead on a contract of employment.
So the concentration I asserted would have been an argument against this paper’s own mechanism, and the variance is what makes commissioning the right instrument rather than a decorative one. The objection improves §6 by removing a claim that undercut it.
One qualification, so the strong form is not carried further than it goes. A famous open problem is the worst case for this, not the best: the extreme tail is where accumulated context matters most, and a posted obligation is not that. The unit in §3 is a bounded, named statement — and it is precisely there that an unexpected closer is plausible, because a bounded problem admits a fresh approach and does not require the decades of orientation an open-ended one does. The mechanism does not need anyone to solve a Millennium problem. It needs the closer of a named obligation to be someone the poster could not have named in advance, which is a much weaker and much more likely condition.
There is also a reason the useful-work variant has repeatedly failed, and it is not incidental. Bitcoin’s work is deliberately useless, and that is a design requirement. Work with an external use has an external demand curve, so the protocol no longer controls the incentive: the participants optimise for the outside buyer, and the security budget decouples from the reward. Every scheme that has tried to redirect mining toward useful computation has met this. A theorem is the most externally useful thing on the list, which makes it the worst possible proof-of-work.
A finite, non-renewing supply is not a mine. It is an extraction, and extraction economics run the other way: the marginal cost rises as the accessible ones go, so the throughput falls exactly as the scheme matures.
Except that mathematical obligations do not behave that way either. Closing one typically opens several — that is what a proof does. The seam regenerates. But it regenerates by mathematics, not by protocol, and no difficulty algorithm has any say in it. Which locates the actual generator of demand precisely, and it is not the reward schedule.
It is whoever posts obligations. That is already the unit in §3, and the objection turns out to strengthen it rather than replace it: demand here is constructible, and the construction is commissioning rather than mining. A buyer creates demand by naming a statement they want discharged, which is the same act that makes the market ungameable. One mechanism does both jobs, which is usually a sign the mechanism is the right one.
And the party with the most to post is the one already holding 275 of them. MEASURED
If one party both posts and pays, volume can be manufactured. Post easy obligations, close them, exhibit the throughput. Every clause of §1 still passes — the before-state is observable, the closure is real, the kernel is satisfied — and the number means nothing. This is WP-75’s inflated-baseline failure arriving through a different door: not a false claim, a true claim about a chosen quantity.
The defence is that poster and closer must be different parties, and that is a governance requirement rather than a technical one. Nothing in the kernel enforces it. It is the one place in this design where the verification instrument does not do the work and a person has to, which is worth stating plainly rather than discovering later. OPEN
Whether anyone pays is not established here and this note does not predict that they will. OPEN
It does not claim a market exists, that one will, or that any instrument should be built. It designs no token, endorses none, and is not investment or financial advice.
It does not claim that formal mathematics is where the important mathematics happens, nor that an obligation worth posting is the same as a question worth asking. §4 is explicit that the second judgement is not mechanisable and stays with a person.
And it does not claim novelty for paying people to prove things, which is old — prizes, bounties and commissioned proofs long predate any of this. What is new, if anything, is the criterion in §1 being satisfiable at all, and the asymmetry in §2 running the right way for once.