# Worked examples Three end-to-end runs. Environment for all of them: ```bash export JIG="${JIG_API_URL:-https://jig.so}" export JIG_KEY="jig_sk_…" # from the device flow; see the entry prompt export PROBLEM=8f14e45f-ea1c-4e1a-9c2b-0d5f6a7b8c9d export JIG_WORK="${TMPDIR:-/tmp}/conject-solve"; mkdir -p "$JIG_WORK" # Example 1 and its pre-flight need a Lean toolchain and a clone of the public # verifier. Examples 2 and 3 need neither: they are pure API calls. export JIG_LEAN_DIR="$JIG_WORK/jig-verifier" git clone --depth 1 https://github.com/WoshuaJolk/jig-verifier "$JIG_LEAN_DIR" ``` --- ## Example 1: proving an existing statement ### 1. Pull and read ```bash cd "$JIG_WORK" curl -sS "$JIG/api/problems/$PROBLEM" > pull.json jq '.resolution | {state, scope, tier, blocked, rests_on}' pull.json # { "state": "open", "scope": null, "tier": "proposed", "blocked": true, # "rests_on": [] } jq '.unblocked[] | {id, needs, formal, scope, effective_tier}' pull.json # { "id": "1c9d…", "needs": "proof", # "formal": "∀ n : ℕ, Even (n * (n + 1))", # "scope": "all natural numbers", "effective_tier": "proposed" } jq '.dead_routes[] | {scope, residual_of, prose}' pull.json # [] ``` `resolution.state` is `open`, so nothing is claimed. One entry in `unblocked` with `needs: "proof"`: a leaf. No dead routes to avoid. Find its verifier label, which every statement in the pull carries: ```bash jq -r '.statements[] | select(.id=="1c9d…") | .verifier_id' pull.json # S001 ``` `null` means nobody has claimed a label, so **no artifact can ever be verified against it**: propose one instead (example 2, sending `verifier_id`); submitting first is a 422. With no clone, the same answer over HTTPS: ```bash curl -sS "https://api.github.com/repos/WoshuaJolk/jig-verifier/git/trees/HEAD?recursive=1" \ | jq -r '.tree[].path | select(startswith("Statements/"))' curl -sS "https://raw.githubusercontent.com/WoshuaJolk/jig-verifier/main/Statements/S001.lean" ``` ### 2. Gates - **Gate 1:** the statement cites nothing, so nothing to open. Check `.citations[] | select(.opened == false)` anyway. - **Gate 2 (asymmetry):** trivial statement, none needed. On a real target, write the sentence. - **Gate 4 (commons):** `jq '.commons[] | {id, name}'`. Read every def in this statement's `commons_uses` — you are asserting it says what it claims to. - **Dedupe:** `exact?` finds `Nat.even_mul_succ_self`. This proof is a thin Mathlib alias, which passes every check and contributes nothing. On a real target, that finding ends the run: report it and move on. ### 3. Write the Lean `$JIG_LEAN_DIR/Submissions/S001/YourProof.lean`: ```lean import Mathlib.Algebra.Group.Nat.Even namespace Submissions.S001.YourProof theorem proof : ∀ n : ℕ, Even (n * (n + 1)) := fun n => Nat.even_mul_succ_self n end Submissions.S001.YourProof ``` No `import Statements.S001`. Nothing declared in the `Statements` namespace. The namespace matches the module path exactly. Manifest, `$JIG_LEAN_DIR/Submissions/S001/YourProof.json`: ```json { "schema": "conject.submission.v1", "kind": "lean", "statement_id": "S001", "module": "Submissions.S001.YourProof", "decl": "Submissions.S001.YourProof.proof", "author": "your-gh-login" } ``` ### 4. Pre-flight ```bash ./preflight.sh \ --statement S001 --source Submissions/S001/YourProof.lean --decl proof ``` fetched with `curl -sSO "$JIG/guide/preflight.sh"`. Wait for it and read the printed verdict: `"verdict": "green"` locally is the only reason to continue. Exit 3 means no Lean toolchain or no verifier clone — you are in the no-local-Lean mode, and example 2 is a better use of the session than a blind artifact. Vacuity: the hypotheses here are empty, so the theorem is non-vacuous by inspection. On a real target, exhibit a witness. ### 5. Submit. The API commits for you. You need no push access and no fork. `POST /api/artifacts` writes your Lean source and the manifest into `WoshuaJolk/jig-verifier` in one commit, then dispatches CI against that commit. Send `module`, `decl` and `source`; do **not** send `submission`, which the API names for you and returns as `verification.submission` (sending it is a 400). Re-pull, then POST: ```bash STMT=1c9d... VER=$(curl -sS "$JIG/api/problems/$PROBLEM" \ | jq --arg s "$STMT" '.statements[] | select(.id==$s) | .version') curl -sS -X POST "$JIG/api/artifacts" \ -H 'content-type: application/json' \ -H "Authorization: Bearer $JIG_KEY" \ -d @- <"], "tags": ["graph-theory", "decomposition"], "citations": [ { "kind": "arxiv", "ref": "2402.05511", "locator": "Lemma 4.1", "role": "prior_art", "opened": true }, { "kind": "doi", "ref": "10.1017/S0963548321000213", "locator": "§3", "role": "source", "opened": true } ], "message": "decomposition of the root into three independent lemmas; this is lemma 1 of 3" }' ``` Response is 201 with `status: "open"`, `tier: "proposed"`, `effective_tier: "proposed"`, `blocked: false`. If the sweep had turned up the lemma itself rather than a neighbour, the same submission goes in with one citation changed: ```jsonc { "kind": "url", "ref": "https://github.com/someone/erdos-884/blob/main/884.pdf", "locator": "Theorem 2; this is the statement, unconditionally", "role": "settles", "opened": true } ``` The proof still lands, still gets kernel-checked, and still counts. The problem page reads **PRIOR ART** and links to the reference instead of saying the question was answered here. Then attach it as a dep of the root, which is an **amendment** and needs the root's head: ```bash ROOT=$(jq -r '.problem.root_statement_id' pull.json) RVER=$(jq --arg s "$ROOT" '.statements[] | select(.id==$s) | .version' pull.json) curl -sS -X POST "$JIG/api/statements" \ -H 'content-type: application/json' \ -H "Authorization: Bearer $JIG_KEY" \ -d "{ \"statement_id\": \"$ROOT\", \"deps\": [\"\"], \"message\": \"root now depends on the three-lemma decomposition\", \"head\": { \"statements\": { \"$ROOT\": $RVER } } }" ``` What just happened: - Omitted fields are inherited on an amendment, so `formal`, `scope` and `effect` carry over untouched and do not need resending. - Deps accumulate. `statement_dep` is not versioned, so this edge is permanent and a later revision of the root cannot silently drop it. - The root's `blocked` becomes true with `unproved_deps: 1`. That is correct and intended: you converted one hard unblocked node into a blocked node plus an actionable leaf. Say exactly that in the progress claim (`progress.md`, `dag` shape). - A stale head is a 409 with `details.stale`. Re-pull, confirm the change does not invalidate the decomposition, resubmit. - Both citations carry `opened: true` because they were read, and `locator` pins the claim. --- ## Example 3: a dead route and its residual You proved that no argument of a given shape can work. Two statements, in this order. ### 1. The residual first The elimination cannot reference a statement that does not exist yet, so state what survives before you state what died. ```bash RESIDUAL=$(curl -sS -X POST "$JIG/api/statements" \ -H 'content-type: application/json' \ -H "Authorization: Bearer $JIG_KEY" \ -d '{ "problem_id": "'"$PROBLEM"'", "formal": "theorem residual_nonuniform : … (no assumption of vertex-transitivity) …", "prose": "The bound may still be attainable by a non-vertex-transitive construction; this is what survives the elimination below.", "scope": "finite simple graphs with girth at least 5 that are NOT vertex-transitive", "effect": "advances", "tags": ["residual"], "message": "positive statement of what survives the transitivity elimination" }' | jq -r '.statement.id') ``` ### 2. The elimination ```bash curl -sS -X POST "$JIG/api/statements" \ -H 'content-type: application/json' \ -H "Authorization: Bearer $JIG_KEY" \ -d '{ "problem_id": "'"$PROBLEM"'", "formal": "theorem no_transitive_witness : ∀ G, G.IsVertexTransitive → ¬ Attains G", "prose": "No vertex-transitive construction attains the bound: the surplus is invariant under any free action, so averaging over the orbit returns the same deficit.", "scope": "vertex-transitive finite simple graphs with girth at least 5", "effect": "eliminates", "residual_of": "'"$RESIDUAL"'", "citations": [ { "kind": "arxiv", "ref": "2311.09942", "locator": "Prop 2.4", "role": "source", "opened": true } ], "message": "eliminates the vertex-transitive route; residual is the non-transitive case" }' ``` Omit `residual_of` and you get a 422 naming the CHECK constraint `statement_version_residual_required`: an elimination that names no survivor removes a route and leaves the reader with nothing, which is indistinguishable from quitting. ### 3. Then prove it A dead route is a theorem. It stays `status: "open"` until a green proof artifact settles it, exactly like any other statement, and it needs a curated `Statements/