Agent frontends

1.1 What each client can send

Whether we can send a value turns out to be a property of the harness rather than of the server, and the harnesses differ more than I expected.

Open WebUI is the one that actually fits the shape of the problem, which is not what I expected from its strata of Node packages and weird version requirements. The unit is a model preset: a base model plus a system prompt plus a pinned parameter set, saved as its own entry in the picker. So one base model can carry several presets — the same weights appearing twice in the picker, a Qwen3.6 at temp 1.0 for thinking beside a Qwen3.6 at 0.6 for coding — which is precisely the distinction the model tables draw and that neither a server-side registry nor Goose can express. It also reads /v1/models, so the model list cannot drift out of sync the way a hand-maintained one does.

A preset is one row in webui.db, and the part that matters is small:

{
  "id": "cascade-2-maths",
  "base_model_id": "nemotron-cascade-2",
  "name": "Cascade-2 (maths)",
  "params": { "temperature": 1, "top_p": 0.95, "min_p": 0.02, "repetition_penalty": 1.05 }
}

That preset mechanism turns out to be a better reason to run Open WebUI than the rendering I originally chose it for. What it looks like against one particular local server — including a parameter name that silently does not survive the trip — is on the Mac page.

5.1 Rendering notation

Hosted clients render LaTeX without our help, so this only bites self-hosted frontends, and there it bites in two places: delimiters and streaming. Delimiters first. Models like to emit \(…\) and \[…\], while most chat UIs only wire $…$ and $$…$$ into their renderer, so the equation arrives as raw backslashes. The fix is a system-prompt line telling the model to emit dollar delimiters; Goose, OpenCode, and Jan all need it. Open WebUI does not: its KaTeX pass registers every delimiter style — $…$, $$…$$, \(…\), \[…\], even \begin{equation} — behind guards that keep prose dollar signs out of maths mode.¹ Qwen-Agent attacks it from the other end: its Gradio UI lets us register the delimiters at the renderer (gr.Chatbot(latex_delimiters=…)) instead of nagging the model. Streaming is the second fumble.²

5.2 Calling the oracle

Reaching a solve() oracle reduces to MCP versus skills, which every row in the table answers the same way, so it decides nothing between them. The one frontend-level trap is the timeout: a synchronous solve() that fans out for three minutes will exceed some clients’ tool-use time limit, which is what the async handle pattern is for.

5.3 Lean state

No chat frontend renders Lean proof state, so this question has one good answer and it is not a chat UI. The Lean 4 web editor runs a Lean server with a live goal panel, so we keep it open beside the chat rather than build our own. When we own the loop we at least see what the loop sees: the compiler’s complaints are the loop’s food, and printing them is free. A custom React app with an embedded editor buys full control for a day or two of plumbing; I’d live in Open WebUI first and defer that until the loops earn it.

5.4 Our loop behind Open WebUI

Owning the loop is one thing, but building a whole new frontend sounds tedious. Fortunately we need not do both. Open WebUI straddles two layers — it is frontend and harness — and the two come apart, so we can keep the frontend and replace the harness underneath it. That is, we can run our own orchestrator and still inherit the KaTeX rendering, the RAG, and the chat history without writing any of it. There are three extension points that seem appropriate, in order of increasing maintenance burden:

• A Pipe Function is the basic option: a Python function that registers as a custom “model” in the chat dropdown, intercepts the prompt, and returns whatever the function produces. Enough for a single custom agent.
• A Pipeline is similar but elaborated: a standalone Python service that Open WebUI talks to as if it were a model, so, for example, the generate-run-verify loop (routing, retries, fan-out, the oracle call) can run in a separate process. Upload a .py file, or point it at a raw GitHub URL, and it shows up as a model in the UI. Looks like enough power for the current purpose.
• MCP (native since v0.6.31) is to let the loop itself use tools — the mathx oracle, a (wrapped) Lean server. It can compose with either of the above.

Logical escalation: keep the stock UI, put the loop in a Pipeline, integrate more needful tools via MCP. I suspect we can defer the custom React app until we hit something outside the scope of Open WebUI, such as proof-state rendering.