proof of work, except the work is real
We mine
truth.
compute resolves a candidate · a kernel checks it · a false truth does not typecheck
Bitcoin spends compute to mine hashes
that prove nothing.
We spend compute to mine things
that are true.
The verifier is a kernel, not a vote.
It cannot be fooled.
Expensive to produce. Trivial to check. Impossible to fake. No partial credit, no consensus to bribe, no oracle to capture.
Compute mines it. A false truth
does not typecheck.
This is a new primitive. Proof of work where the work is real knowledge, manufactured and certified at scale.
the proof it is real · this happened
In one night, a fleet mined a 25-year-open problem.
The target was , the open question behind a $1M Ethereum Foundation prize. Around 150 Lean bricks came back: kernel-checked theorems, honest refutations, and an audit-guard that caught its own false positives. When the kernel rejected a claim, the fleet reversed it. Every accepted result typechecked.
the first mined truth → deltastar.computerEvery accepted result passed the Lean kernel. Not probably right. Checkable by anyone, in one command.
The deep wall stays open. was localized, not the whole prize. The guard refused to let the fleet lie about it. That refusal is the point.
the frontier
Anywhere a cheap trustless verifier exists, truth is mineable.
Mathematics is the beachhead, where the verifier is perfect. From there the frontier expands: cryptographic code, then everywhere a verifier can be made cheap and trustless. Not everything is mineable yet. That boundary is real, and it is the line we push.
mathematics
perfect verifier · proven
cryptographic code
cheap trustless verifier · next
the open frontier
wherever a verifier can be built
Bring a target.
We mine it.
build · commission · get in touch · github.com/lalalune/ArkLib