Ansatz

Ansatz is a reasoning instrument you open from the Composer with the /ansatz slash command. It replaces the panel with a terminal over a run: a set of claims, the evidence and verification artifacts filed against them, and the reviews that close them out. Each claim’s epistemic state is computed from that history rather than set by hand.

Opens with

/ansatz

Exit

Esc

Command bar

:

Note

Ansatz is early. It ships with a seeded demo run so the terminal works before a space has a run of its own, and some commands are refused on that demo world. The status bar tells you which world you are in.

Opening and leaving

Type / in the Composer input and pick Ansatz, or type /ansatz. Unlike /summarize, this command never reaches the chat socket: the terminal is a client-side overlay. Esc exits and puts the workspace back exactly as it was.

If you have a space open, the terminal attaches to that space’s run or creates one. Without a space, it falls back to the seeded demo run.

Views

Seven views, selected with the number keys 1 to

7, or by clicking the tabs:

session graph warrant routes obligations review run

G jumps to the graph and ? opens help,

which lists every command with its usage line.

Epistemic states

Every claim carries one state, shown as a glyph:

Glyph	State
?	conjectured
~	explored
✓	supported
!	challenged
✗	refuted
✓✓	human_verified
⊢	machine_checked
⊨	formally_verified

State is a fold over the run’s claims, artifacts, and reviews. No command sets a state directly. That has one consequence worth knowing before you use :edit: editing a claim’s statement bumps its version and strands every artifact filed against the old text, dropping the claim back to conjectured.

Commands

Press : to open the command bar. Arrow keys walk your history, ↵ runs, Esc closes the bar without leaving the terminal.

Command	What it does
:claim [@route] <statement>	Mint a claim, optionally on a route
:ob @route <statement>	Mint an obligation on a route
:route <title>	Open a new route
:link <from> <predicate> <to>	Typed edge: premise_of, refutes, supports, analogous_to, formalizes, decomposes_into
:evidence <claim> <subtype> <summary>	File evidence: numerical, literature, generated, counterexample, challenge
:edit <claim> <statement>	Edit a claim, stranding its artifacts
:sweep <claim> <expr> ; x=lo..hi [int] [steps=N] ; tol=1e-9	Deterministic counterexample sweep
:lean <claim>	Open the Lean composer
:accept <claim> [note]	Record human acceptance
:dismiss <artifact> [note]	Dismiss a challenge or counterexample
:status <active|dormant|closed> [reason]	Set the run status

:help or :? lists the same table in the terminal.

Sweeps

:sweep runs a deterministic grid search for counterexamples. Declare one or more variables after a semicolon, each as either a range (x=0.001..0.1) or an explicit list (n=2,4,8), with optional int and steps=N flags, and an optional tol= tolerance chunk. The result reports violations against samples, the worst slack when clean, and a witness assignment when not.

Lean checks

:lean <claim> opens a composer pinned to that claim’s current statement hash. Write Lean 4 source and submit with Ctrl+↵, or cancel with

Esc.

The check is a real compile on the server against a Lean toolchain, run under the strongest sandbox the host offers, and it is debited against the run’s Lean seconds budget. sorry never passes. A passing check earns ⊢ machine_checked at most: ⊨ formally_verified additionally requires the faithfulness review, which asks a human whether the Lean statement actually formalizes the claim.

In the review view, A accepts and R rejects the oldest pending faithfulness decision.

Live runs versus the seed world

The right side of the status bar shows ⚡ live when the terminal is attached to a backend run and ◌ seed when it is on the built-in demo world. On a live run every command is a POST to the server’s validator, which is the only writer, and the terminal re-reads the world from the run’s event log afterwards. On the seed world the same fold is applied locally so the terminal stays usable offline.

Sweeps and Lean checks are refused on the seed world, since both are backend capabilities.

The rest of the status bar shows the live routes, a census of claim states, artifact calls against the run’s budget, the round number, and the run status.

Read nextComposerWhere /ansatz is typed, and the rest of the slash commands.