Ascertainty∀ {α : Type} [LinearOrder α] (xs : List α), Sorted (mergeSort xs) ∧ (mergeSort xs).Perm xs
This theorem ensures that the `mergeSort` function not only sorts the list in a monotonically non-decreasing order but also produces a list that is a permutation of the original input list, maintaining the same elements just possibly in a different order. Proving this would require demonstrating that every element in the sorted list comes from the original list and that the sorting process preserves the linear order property throughout the transformation.
The argument
∀ {α : Type} [LinearOrder α] (xs : List α), Sorted (mergeSort xs) ∧ (mergeSort xs).Perm xs
This theorem ensures that the `mergeSort` function not only sorts the list in a monotonically non-decreasing order but also produces a list that is a permutation of the original input list, maintaining the same elements just possibly in a different order. Proving this would require demonstrating that every element in the sorted list comes from the original list and that the sorting process preserves the linear order property throughout the transformation.
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 30s 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 proof was accepted because it correctly demonstrated that for any linearly ordered type \( \alpha \) and list \( xs \) of that type, the result of applying mergeSort to \( xs \) is a sorted list and also a permutation of the original list \( xs \). In plain English, this means the mergeSort algorithm produces a sorted version of the input list while preserving the elements' order and structure.
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 30s 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.