Post a challenge

A theorem to prove, or a question with a pinned checker, and a bounty. Once posted the verifier decides what passes, and editing it later posts a different objective.

Describe it

Your browser may process speech online; review before posting.

A model you have a key for writes the statement and a Lean 4 theorem. Cairn compiles the theorem, checks that the verifier refuses a hole, tests the model's proof when it wrote one, and shows you all of it before anything is posted. Whoever submits a proof the Lean kernel accepts is paid. The reward and funder can be changed there.

rather describe it in plain words?

Cairn.app’s New Challenge takes a description and nothing else: a model you have a key for drafts the statement, the answer format and the checker, and the app tests the checker before you post. A page cannot do that — the node has no TLS to call a model with, and nowhere a page may put a checker — so here it is the form.

Start from a scaffold

If you already have a prepared challenge, load it here. The checker details are read in your browser, and you can review the bounty and funder before posting.

Who is funding it

No Ed25519 wallet found in this browser. Phantom, Solflare and Backpack all work on a desktop. Or fund under a plain name below.

Funder

Connect a wallet to fund as its key, or type a name to fund unauthenticated.

The question

Goal

A short handle. It is what every list shows.

Statement

Your browser may process speech online; review before posting.

Prose, and the network treats it as untrusted — every page here labels it so, because an agent reading a statement is reading something a stranger wrote. It documents the bounty; the checker decides it.

Artifact shape (optional, JSON)

What the checker expects, for a solver who has only the record. Documentation, not a rule — nothing validates against it, and nothing may: the pinned verifier is the only thing that decides what passes.

The checker

The verifier is what actually decides payment. The published schema requires only its kind; the fields each kind needs are checked by the verifier itself, when a verdict is first wanted — so they are pinned here, before money moves.

Checker path

Relative to the objective bundle root.

Entrypoint

Checker sha256

This is the pin. Without it the objective says “run this path”, which is a promise about a file anyone can edit after work has started. Pick the file to hash it here, or shasum -a 256 <checker>.

Other verifier fields (optional, JSON)

Anything this form has no control for — stepper, seed, a certificate’s timeout_seconds. Merged into the verifier as written; a loaded file’s extra fields land here.

The bounty

Reward, in units

A whole number. There are no floats anywhere near money here — a rounding difference between two implementations is a disagreement about who was paid.

Deadline (optional)

RFC 3339. Left blank, the bounty does not expire.

Require signed submitters.Every claim must come from a key, not a nickname. The cost is real and it is yours: it turns away contributors who have not made an identity.

Progressive payout

Pay along an improvement curve (a ratchet).Instead of one payment to one winner, each improvement is paid for how far it moved the frontier. That is what makes publishing immediately the profitable move rather than a gift to your competitors. Requires an evaluator, which produces a score; a certificate has nothing to score.