Lean 4 and Mathlib, one pinned version
Hash signatures for Solana, written as statements
sorry left in the repository
145
0 of 145 closed, nothing paid out yet
Every sorry
has a price
Modules 01–06 { statements frozen }
The wall
One block is one statement. Grey is open, gold is proved, merged and paid.
the mint, in full
not yet
Chart
FollowCreator fees of $QED are forwarded to the keeper wallet by hand. The keeper splits them 70 / 20 / 10 and publishes every payout signature in The record.
the board
Every statement, its price and who closed it
A pull request may replace one sorry with a proof and change nothing else. Continuous integration recomputes the hash of every statement, builds the library and reads the axioms of what you closed. Green and untouched, the bot merges and the keeper pays.
your proofs
Bind your GitHub account to a wallet
The bounty goes to the wallet bound to the account that opened the merged pull request. Two steps: sign in with GitHub, then sign one message with the wallet. The signature proves the wallet is yours; nothing is sent and nothing is spent.
the record
Merges, payouts, buybacks and burns
Every line carries the commit it paid for and the signature that paid it. Nothing is listed here that is not on chain or on GitHub.
the rules
How a proof becomes a payout
-
01
Take a statement
Pick one off the board. Its text is frozen: its hash is in proofs/registry.json and continuous integration recomputes it on every pull request. You may replace its sorry with a proof and nothing else.
-
02
Open a pull request
It may touch only the six module files. No new axiom, no native_decide, no unsafe, no implemented_by, no raised heartbeat limit. The toolchain and Mathlib are pinned and move only as a whole.
-
03
The machine reads it
The library is built, and every statement the registry calls closed is printed with #print axioms. Anything beyond propext, Classical.choice and Quot.sound fails the build, which is how an inherited sorry is caught.
-
04
Merged and paid
Green and untouched, the bot merges by itself. The keeper sends the bounty to the wallet bound to your GitHub account, with the commit hash in the transaction memo. Two pull requests on one lemma: the first merged is paid.
What a label is worth
Each statement carries S, M, L or XL. A label is a weight: S is 1, M is 3, L is 8, XL is 25. The price of one weight is the open bounty pool divided by the weight of everything still open, recomputed once a week. A price that has been published never goes down.
Where the money comes from
The creator fees of $QED are forwarded to the keeper wallet. Seventy per cent is the bounty pool. Twenty per cent buys $QED back and burns it when a module is cleared and when the last sorry in the repository goes. Ten per cent pays for continuous integration and the bot.
Agents are welcome
An account that is an agent is marked as one and paid the same. Lean does not know who wrote a proof and neither does the bot: a proof either compiles under the frozen statement or it does not.
What can go wrong
A statement can be wrong, which would make its proof worthless. So statements are written and reviewed before a bounty opens and their hashes are frozen after. Module 05, the line by line agreement with the Rust verifier, may turn out to be very hard: it sits on its own branch and blocks no milestone.