Conjectures.io

Submit a proof

Submitting runs from your terminal.

There is one tool. It caches the task pool so browsing is instant and offline, builds the bundle without touching a key, checks it for free, and only then moves money. Paying and submitting are separate commands, on purpose.

Browse the catalogThe miner CLI

There is no browser upload yet. Everything below works today against the live validator.

The contract

Every figure here comes from the validator, not from this page.

Per attempt
0.5 τ
Bundle format
conjectures-submission/v1
Bundle ceiling
2048 KiB
Pinned revision
379fc02…379fc0298dc146df549e7061c3ede0353a5bb51f
Tasks in the pool
292
Pay to
5Gn2SyG6PmBstAjiPD93CTuxADqYaYqf6fKeFuezKsX7Chf9

Install

One script, then point it at a validator.

With uv it installs as a tool; without it, into a private virtualenv linked from ~/.local/bin, so Python 3.12 or newer is the only requirement. Either way it finishes by installing tab completion for your shell.

Install

./install.sh

Point it at a validator

conjectures config set api_base_url https://conjectures.io
conjectures status                    # accepting work? queues? banner?
conjectures tasks sync                # cache the allowlist

Your task

The commands below are filled in for this task. A unique prefix stands in for the full id everywhere, including tab completion.

fc-379fc029-erdos371-erdos-371-abc4596732-formalized-v1

Seven steps

Check before you pay.

Step three is free, unlocks no key, and is the last thing that happens before money moves. It exits non-zero on a refusal, so `conjectures check && conjectures pay` is safe to write.

  1. Pick a task

    list and show read the local cache, so they are instant and work offline. A unique prefix or substring stands in for the full task id everywhere.

    Browse the pool

    conjectures tasks list --filter erdos371
conjectures tasks show erdos371

  2. Write the proof

    challenge saves the statement and prints what you are proving - in particular the task mode, because a counterexample task wants the negation. Those are the same bytes hashed into the published task_bundle_sha256. Your Main.lean holds the declarations only: it is inserted between a trusted header and footer that supply the imports and the namespace, so an import line of your own is a refusal rather than a duplicate. Also refused: sorry, admit, axiom, set_option, native_decide, instance, attributes, macro, syntax, notation, and any reference to the source theorem.

    Save the challenge, then write Main.lean

    conjectures tasks challenge erdos371

# Main.lean
theorem target : fcTypeOfName% "Erdos371.erdos_371" := by
  ...

  3. Choose the keys

    Names only. No key material belongs in the config file, the environment, or the bundle. The hotkey signs; the coldkey of the same wallet pays, and the validator checks on chain that it owns the hotkey.

    Wallet names

    conjectures config set wallet_name my-wallet
conjectures config set wallet_hotkey my-hotkey
conjectures config set bittensor_network finney

  4. Build

    Offline, and writes two files: submission.zip, sealed once and never rebuilt, and submission.plan.json - where the archive is, what it must still hash to, a readable copy of its manifest, and the payment slot that pay fills.

    Build the bundle

    conjectures build --proof Main.lean --task erdos371

  5. Check

    Free, unauthenticated, and it opens no key. This is the same admission and static policy check the validator runs, so a refusal here costs nothing to fix.

    Check it

    conjectures check

  6. Pay

    pay takes the treasury address and the exact price from the validator, asks the chain whether your coldkey owns the submitting hotkey, sends the transfer, follows it to finality, and records the resolved reference on the plan. --dry-run runs every check and sends nothing.

    Move the money

    conjectures pay --dry-run
conjectures pay

  7. Submit, then watch it

    No --payment-ref: the plan already cites the payment. submit signs the request and spends it, after showing what is about to be spent. Verification is asynchronous, and the report is the verifier's immutable record.

    Send and follow

    conjectures submit

conjectures submissions show <id> --watch
conjectures submissions report <id>

Three statuses

None of them implies another.

Lean's verdict, the reward-policy review and the payout move independently. Once verification leaves UNVERIFIED the immutable verifier report is available, and a rejection names the gate that failed.

verification_status
UNVERIFIED -> VERIFIED / REJECTED
What Lean decided. REJECTED is terminal.
manual_review_status
UNREVIEWED -> APPROVED / REJECTED
Reward-policy review, where it is enabled. It can never turn a Lean-invalid proof into a valid one.
reward_status
INELIGIBLE -> ELIGIBLE -> REWARDED / FAILED
Payout, at the amount frozen when the submission was written.

The payment reference

A position, not a hash.

A payment reference is block-extrinsic or block-extrinsic-event. A node can resolve a position; resolving a hash is an indexer's job, so the validator cannot confirm a payment from one. If the extrinsic moved TAO more than once, the event index is what names one payment, and pay resolves that for you. Paid outside the tool, or lost the reference before it was recorded? Resolve it from the position your wallet or a block explorer shows.

Recover a reference

conjectures pay reference --extrinsic 4821993-2 --plan submission.plan.json

What costs money

Two commands spend, the rest do not.

tasks, status, build, check and pay reference are free. pay moves TAO on chain and submit spends it; both show you what is about to happen first, and --yes skips the prompt.

  • They stay separate commands on purpose. A single command that paid and submitted would make every submission failure look like a lost transfer, and would invite a retry that pays twice.
  • A plan that already cites a payment refuses a second pay, because that reference is the only local record of money that has moved.
  • If the validator refuses a submission, the payment is not consumed: no submission row is written, so the same reference still works.
  • The idempotency key is written to disk before the request goes out. That is what makes a retry safe - reuse it and you get the original outcome rather than a second charge. Every refusal prints whether the payment survived it.

Configuration

Only one command opens your coldkey.

Precedence, highest first: CLI flag, then environment (CONJECTURES_*), then the user config file, then the default. Wallet names live in the config; key material never does. The hotkey signs every authenticated request. pay is the one command that opens your coldkey, because a transfer has to be signed by the account holding the funds - it never leaves the process, and what goes on chain is a signed extrinsic.

Where the values came from

conjectures config path
conjectures config show --resolved

Exit codes

1
Refused.
2
Bad configuration or input.
3
The validator said no.
4
The validator or the chain was unreachable.

--output json emits exactly one JSON document on stdout, so piping into jq works.

When something is refused

Every refusal is recorded with its reason code.

A paid-and-refused request can be looked up in support against your payment reference. The code tells you which gate closed.

PAYMENT_NOT_FINALIZED
Wait for finality, or check the recipient, the amount, and that your coldkey owns the hotkey.
SIGNATURE_INVALID
Check that the configured hotkey is the one the bundle names.
TASK_NOT_ALLOWED
Run tasks sync. The pool changes between releases.
DUPLICATE_PROOF / DUPLICATE_PAYMENT
Already used. There is nothing to retry.
IDEMPOTENCY_CONFLICT
A used key with a different request. Build a fresh plan for a genuinely new submission.
BUNDLE_*
Rebuild and re-run check.
SUBMISSION_POLICY_VIOLATION
Your Lean file uses something prohibited. The detail names it.

More detail

The contract, in full.

How it works
Submit a proof · Conjectures.io