Ascertainty\u2200 (\u03B5 : \u211D) (h\u03B5 : 0 < \u03B5), \u2203 (W : \u2115\
The argument
\u2200 (\u03B5 : \u211D) (h\u03B5 : 0 < \u03B5), \u2203 (W : \u2115\
Verifier: Lean kernel leanprover/lean4:v4.10.0 · deterministic, no human in the loop.
Mathlib SHA: 5b1c4e7 — the proof must check against this exact pinned commit.
Settlement: after the 600s challenge window expires with no challenge, settleBounty(bountyId) is callable permissionlessly. USDC always flows to the recorded solver, never to the caller.
Evidence on file
each row is a kernel-checked submission. accepted attestations anchor on 0G Storage; the merkle root surfaces on-chain at submission time.
awaiting first submission
connect a wallet below to be the first prover on this claim. the kernel is impartial · early submission, late submission, same threshold.
The course, generated.
the spec's dependency depth, branching, and hardness are compiled into the track itself. provers race the same path — the shape of the proof becomes the shape of the run.
awaiting first prover · the track is drawn, the line is open.
Settlement authority
after the 600s challenge window expires with no contest, anyone can call settleBounty(bountyId) — USDC always flows to the recorded solver, never to the caller.
KeeperHub's hosted Turnkey wallet on chain 16602 signs and broadcasts the settlement tx.
the wallet that will pay gas + sign the on-chain tx. clickable to the Galileo block explorer for independent audit.
the contract function. KH downtime can't strand the payout — the function is public and any third-party keeper could drive it equally.
File a proof
connect a wallet, paste a Lean proof, sign the EIP-191 message. operator pays gas; the recovered address becomes the on-chain solver of record.