Skip to content
Rex St. John
demolive

Challenge Vaults

Bounties on unsolved mathematics, paid out by proof. Ten open Erdős problems locked in vaults, each stated in Lean, each opened by the first submission the Lean kernel accepts.

Lean / Claude Code

Demo

Problem

Proof of work pays for guessing. Enormous compute goes into puzzles whose only property is being hard, and every scheme that has tried to redirect it at useful work has foundered on verification: you cannot cheaply, exactly and objectively check that the useful thing was done.

Solution

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, and the first submission the Lean kernel accepts opens the vault and records permanent credit for whoever wrote it.

Four checks have to pass: the statement hashes to the one locked in the vault, so nobody claims a block by proving something easier; there is no sorry; nothing leans on a non-standard axiom; and the kernel type-checks the actual proof term.

Analysis

Declaring your result as an axiom gets past the first two checks and fails the third, which is the failure worth looking at — it is the one a careless verifier waves 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.

Result

A working simulation of the mechanism, with the kernel feed showing exactly why each rejected submission failed — 118 submissions and 118 rejections on one block in the run shown here.

Every result is simulated and labelled as such on the page. The ten problems are real and were open when it was built.

Screens

  • The demo mid-run on the Erdős–Turán problem, with twelve prover agents working and a kernel feed rejecting submissions one by one with their specific Lean errors
    Block 3, Erdős–Turán on additive bases. Twelve provers working, seven submissions, seven rejections — and the kernel feed naming the exact reason for each one.
  • A submission passing all four kernel checks — statement hash match, no sorry, standard axioms only, and the proof term type-checking — with the block minted to its prover
    What opening a vault takes: the statement hash matches, there is no sorry, only the three standard axioms are used, and the kernel type-checks the term. Thirteen submissions on this block, twelve rejected.
  • A rejected submission showing the axiom check failing in red while the hash and sorry checks pass, with the type-check step never reached
    The interesting failure. The hash matches and there is no sorry, but the proof declares its result as an axiom — so the check fails and the type-check never runs.
  • All ten blocks minted and linked, each labeled simulated result, beside a credit table showing how many blocks each prover opened
    Ten blocks, each linked to the one before and credited to whoever opened it. Every result is labeled simulated, because it is.