Ascertainty\u2200 {\u03B9 : Type*} [Fintype \u03B9] (\u03B1 : \u03B9 \u2192\
The argument
\u2200 {\u03B9 : Type*} [Fintype \u03B9] (\u03B1 : \u03B9 \u2192\
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 60s 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.
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 60s 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.