# Using Qurak from an AI agent

Connect over MCP (Streamable HTTP) at https://qurak.com/mcp with `Authorization: Bearer qk_...`; https://qurak.com/llms.txt covers registration, OAuth and the REST mirror. This document is generated from the same guidance the server sends in its MCP `initialize` result, so it always matches what a connection is told.

## Choosing between the tools


Qurak evaluates .wl-compatible expressions. Choosing between its tools:

- A new mathematical goal, or a large or unfamiliar computation: `plan_computation` first. Free and deterministic, it pre-flights a draft expression's functions, finds matching verified recipes, and returns the goal wrapped in a working method with this connection's actual budget numbers - adopt that as the brief.
- One self-contained calculation: `evaluate` with no session_id. The default; cheapest; nothing persists. Small trial evaluations are cheap and expected - probe before committing to a shape.
- Multi-step work where later calls need earlier state (variables, function definitions, loaded data): `evaluate` with a session_id. Reuse ONE meaningful id per line of work instead of minting a fresh id per call - live sessions are capped per account and the least-recently-used is evicted. Sessions expire after ~30 minutes idle; free one early with `clear_session`. `list_sessions` shows the live ones and `inspect_session` what one defines - the check to make before trusting a predicate on a session variable, since an unbound symbol answers `False` to `OrthogonalMatrixQ` and the like without a word of complaint.
- A chart: `plot` (returns a PNG image). `evaluate` only reports that a graphic was produced.
- Work likely to exceed the interactive compute budget (`get_capabilities` reports it; seconds, by plan): `evaluate_async` queues a background job with a minutes-long budget and returns a job_id at once. Collect it with ONE `get_job` call passing `wait_ms` (a free long-poll that returns the moment the job finishes) rather than a tight polling loop. Jobs are a limited daily allowance, so try `evaluate` first when in doubt - resubmitting a timed-out expression unchanged via `evaluate_async` is the intended recovery. Submit with a session_id to run the job inside that session: whatever it assigns (say `sol = NDSolve[...]`) stays defined there for later `evaluate` calls - the way to hand a long computation's result to interactive follow-up. `cancel_job` stops a job; `list_jobs` recovers a lost job_id, `list_certificates` a lost certificate_id, and `list_evaluations` a lost run_id - the last narrowed by the same filters the History page offers (an expression substring, a date range, the source, the verification verdict), so a past run is findable and citable across sessions. A submission refused at validation - a denied expression, a malformed circuit or export, an unregistered name, a plan that has none - costs no slot; a queued job spends one whichever way it ends, and cancelling it before it starts refunds it.
- A quantum circuit's measurement histogram: `simulate_circuit` (ideal statevector, standard gate set, plan-dependent qubit ceiling). It queues as a background job sharing the daily allowance - collect the counts with the same `get_job` long-poll.
- A Lean 4 proof to certify: hand `check_proof` the theorem's text as `source` and the server elaborates it in a sandbox, stores the export and checks it in one call - no toolchain, and Lean's own errors come back with line and column (free) when it does not compile (`get_capabilities` reports whether this deployment runs the elaborator, under `proofs.elaboration`). Otherwise pass the lean4export closure of the declarations as `export` (`lake env lean4export <Module> -- <decl>`, no export options; the tool description names the exporter rev and the Lean version) and their names. A background job like the others, but pass `wait_ms` and a small closure answers in the same call; otherwise `get_job` returns the verdict with each statement and its axioms, and a `certificate_id` that `get_certificate` resolves - cite that, not the verdict alone. The `prove-a-lemma` playbook is the whole path from a statement to that certificate. `validate_proof` first, with the same inputs: it says whether the submit would be refused, answer `unsupported` or check, and spends no slot. `inconclusive` means the judge did not finish, never that the proof is wrong; `unsupported` names what the checker cannot judge (a `sorry`, a custom axiom, an export outside its format window).
- Unsure a function exists or matches reference behaviour: `check_support` (cheap, batched) before spending an evaluation discovering it; `search_docs`/`get_task` serve verified step-by-step recipes.
- An answer you are about to rely on: `verify` with its `run_id`. It derives a check from the question's own shape - differentiating an `Integrate` back to its integrand, substituting a `Solve` solution into its equation's residual, approaching a `Limit` from both sides, checking a `Series` by how fast its error shrinks - and never re-runs the derivation, so it costs the check rather than the computation. `refuted` means the answer disagrees with an independent route; `inconclusive` means nothing was learned, not that the answer is fine.
- A model worth keeping past the session: `save_guide` stores its definitions, assumptions and conventions durably on the account; `list_guides`/`get_guide` reload them in a later conversation, in any client - load a guide's definition blocks into a fresh session to resume where the model left off. `plan_computation` surfaces matching guides automatically.
- Numbers for pacing - budget ceilings, rate limit, session and job allowances: `get_capabilities`. Read limits there, not from failures.

Timeouts, refusals and quota answers come back as tool results with isError set - read them and adjust; the connection is never torn down for a bad expression. No file, process, network, or natural-language operations exist here.

## Playbooks

Served as MCP prompts for clients that surface them; any other agent can follow the same procedures - each defers to `plan_computation` for grounding.

- `compute` - Start any mathematical goal the grounded way: pre-flight, probe, then commit.
- `long-computation` - Work likely to exceed the interactive budget: background jobs, done properly.
- `working-session` - Multi-step work as a living model: one session, named definitions, cheap follow-ups.
- `plot` - Get a rendered chart out of Qurak, with the data prepared where it belongs.
- `port-from-wolfram` - Migrate existing Wolfram Language code: support split first, divergences verified.
- `verify-numerically` - Cross-check a doubtful or unevaluated symbolic result before trusting it.
- `prove-a-lemma` - From a statement to a citable certificate: the pinned toolchain, the export, one check_proof call.
- `model-a-decision` - Lift a choice between alternatives into a break-even model with sensitivities, instead of a one-number verdict.
- `what-if` - Answer a what-if with now, then, and the per-unit sensitivity - not a guess.
- `fermi-estimate` - A what-would-it-take question, answered by decomposition with exact arithmetic and comparable scales.
- `growth-and-time` - Compounding, doubling times, and when-do-I-get-there - as a model of time and rate, not a single projection.
- `chances` - Probability questions answered three ways: at least once, the expected count, and the tail.
- `fair-price` - Is this deal good - via present value against the alternative, and the rate the deal implies.

## Where the numbers live

Budgets, rate limits and allowances are per plan and enforced server-side: `get_capabilities` reports this connection's own numbers, and https://qurak.com/billing/plans is the machine-readable catalogue. Read limits there, not from failures.