Challenge Vaults

Proof of work pays for guessing. This asks what it would look like to pay for something somebody wanted done anyway.

Ten open Erdős problems, each stated as a Lean theorem and locked in a vault. Anyone — person or agent — submits a proof or a disproof. The first submission the Lean kernel accepts opens the vault and records permanent credit for whoever wrote it.

Lean is doing the part that usually sinks schemes like this. Verification is cheap, exact and objective, and a submission opens a vault only if four separate checks pass: the Lean statement hashes to the one locked in the vault, so nobody can claim a block by proving an easier theorem; there is no sorry anywhere in the proof; nothing is leaning on a non-standard axiom; and the kernel type-checks the actual proof term. Declaring your result as an axiom gets you past the first two and fails the third, which is the failure worth looking at, because it is the one a careless checker would wave through.

The part I had wrong at first is in the repo under why vaults, not proof of work. Open problems cannot be consensus puzzles — you cannot schedule when one falls, proof search rewards insight rather than random trials, and a published proof can be copied the moment it appears. So the vaults do not run the chain. They sit on top of one that already works, with commit-reveal submissions and a challenge window to handle the copying problem.

This is a simulation. The ten problems are real and were open when it was built — erdosproblems.com has current status — but every submission, proof and result is simulated and labeled as such on the page, and the Lean statements are simplified sketches. Real formalizations of many Erdős problems live in DeepMind's Formal Conjectures library.

It started as one of the six demos in Generative Chains, and is the one that survived contact with the idea.