Building a maths agent

1 The path through

Suppose I already use some coding harness. I can proceed step by step to add features, one at a time, walking through harness design space until it is more optimized for mathematics than for code. That space has four axes — wiring (how the calls connect to one another), verification (what gets to say an attempt was any good), context (what each call is shown) and dispatch (which model or tool fills which slot) — and every step below moves exactly one of them, which is what the second column of the table records. Some steps, in a recommended order (I won’t divulge whether I actually followed this order):

These all cost different amounts of effort to build, and yield different amounts of effect. That last column is not my measurement. It comes from AxProverBase (Requena et al. 2026), a deliberately stripped-down Lean-proving agent whose authors assembled it one component at a time and scored each addition separately — the nearest thing to a controlled experiment on any of this that I know of. Ranked by effect, they put iterative refinement first and memory second, which are the third and fourth steps here; building the oracle is nevertheless easier and more fun than either.

I suspect that the table continues past my ability to build. In particular, the recursive, self-grading, re-formalizing orchestrators at the top of the mathematics leaderboard have enough startup money behind them that buying access off the rack is probably the better move.

2 Easy mode

The baseline: an ordinary harness, an ordinary model, no axis moved.

An ordinary agent harness I already use for code, pointed at a good generalist reasoning model, gets me some way toward powerful mathematics. Claude, the latest DeepSeek, or a big Qwen3-Thinking are all respectable mathematicians; tell them to “do the maths”, then “check the working with Python/SymPy”.

This works pretty great with e.g. Claude Desktop, Claude Code etc. NB local clients are less capable at rendering equations, so we may want to build Open WebUI to make equations easier on human eyes.

3 Lend it an oracle

Moves dispatch: one slot in the loop gets filled by a specialist instead of the generalist.

Now we can use our existing agent as an orchestrator, but let it delegate mathematics (or the checking of mathematics) to a specialist maths model. Practically, this means we give it a solve() oracle tool to solve knotty maths problems, splicing the result back into its own reasoning. Oracle in the strict sense: the orchestrator does not attempt the sub-problem and does not check the answer; it asks and then believes, so whatever confidence the tool reports is all the confidence there is.

Python harnesses like Smolagents or Qwen-Agent can simply call a Python function. For other agents (Claude-like, Goose, Codex, Gemini CLI, pi, Hermes) we expose the solve() as a CLI tool. Both of these can be documented by an agentskills.io SKILL.md in skill-supporting agents. Skill-blind agents can use an MCP server.

I whipped up mathx as an example of doing all three, in a relatively swappable manner.

We might wish to fan-out in such an oracle. Done synchronously, this can be slow and hit time limits on tool use, or just get boring. Asynchrony and parallelism depend on the orchestrating agent. When we own the loop, a fan-out is just asyncio.gather, and there is no timeout that we do not ourselves set. For tool-use agents, the async-handle pattern is probably what we want — we set up a handle-and-poll pair of ordinary tools: submit_solve() returns a job id at once and check_solve(id) returns status-or-result at once, so each call is fast. Some harnesses also dispatch background sub-agents of their own, and MCP supports Tasks at the protocol level; that might work too.

4 Build the loop

Moves wiring to sequential: the verdict comes back and we try again.

What iterates is attempts at one problem. Two roles, and the loop is just the two of them passing work back and forth: a proposer, the model that writes a candidate answer or proof, and an executor, whatever runs or checks what the proposer wrote. The proposer writes a candidate, the executor checks it, the verdict — a compiler error, a failed numeric check — goes into the next prompt, and round it goes again until the check passes or the iteration budget runs out (AxProverBase allows 50 rounds per problem). This is not the same thing as fan-out: there the attempts are independent and mutually blind, whereas here attempt \(n+1\) has seen what attempt \(n\) got wrong.

If easy mode plus an oracle aren’t enough, we can write a custom loop that specializes the generic one for mathematical needs. This is the single largest contributor in the AxProverBase ablations, and it is also where the maths usage diverges from the coding usage.

The difference is in the executor: a maths executor by default only ever checks a calculation, which is side-effect-free — fifty attempts cost fifty times the tokens and leave nothing else changed, whereas fifty attempts at a repository leave fifty conflicting sets of edits — and that is what makes fan-out simple.

Two maths-harness gotchas:

• TIR models speak their own tool-call dialect, so the orchestrator has to parse fenced code templates and splice results back in the shape each model expects. Budget for writing that parser per model family; it is the thing that stops a generic harness working.
• The model writes the code we run unobserved, so sandboxing is wise. The only maths-specific detail is that the specialists assume a full scientific Python (SymPy, NumPy), so build the sandbox accordingly.

5 A scratchpad

Moves context: what a call sees now includes what previous attempts learned.

A stateless loop repeats itself forever, and fixing that is the second-largest lever in the whole architecture — behind iterative refinement, ahead of the search tools. It is also cheap to add. This is memory a few turns wide, not the session-and-project kind, and what a maths loop specifically forgets is which lemmas exist in Mathlib and what they are called this month — so it burns its budget rediscovering that Nat.foo was renamed three versions ago. The crude version pastes the whole transcript of past attempts into the prompt, but that bloats the context, makes every call slower and dearer, and eventually overflows the window. The version that works is a short self-managed note: after each attempt the proposer rewrites a running scratchpad of what it learned — which lemmas don’t exist, which tactics misfired — pruned so it never grows without bound. On the AxProverBase numbers, that self-managed note buys around 7% more theorems at ~20% lower cost, with half the run-to-run variance, beating both no memory at all and a rolling transcript of recent attempts. With memory in place — and the library-search tool alongside it — the prover stops re-making the same name and syntax errors, freeing budget for proof search.

6 Fan-out

Moves wiring to parallel: many samples at once, and something downstream to choose between them.

Fan-out improves mathematical accuracy by evaluating many candidate solutions — maj@k or Pass@k, depending on what came back. We can run a lot of these fuckers at once, since the tokens stream over the network in parallel.

The goal here is overall efficiency: do more parallel copies of a cheaper model get us further than fewer copies of a more powerful one?

Asked for \(7^{2026} \bmod 13\), VibeThinker-3B and Ornith-1.0-9B both answered 4, correctly and with sound reasoning. VibeThinker spent 786 completion tokens; Ornith spent 6,316. Multiply by \(k\) and that ratio is the economics of fan-out — a model three times the size costing eight times the tokens per sample is not a near-miss, it is a different budget. So benchmark accuracy picks the shortlist and tokens-per-correct-answer picks the winner.

The cheapest thing to fan out is a model that runs no code at all — a pure chain-of-thought reasoner emits no Python and no Lean, so its executor is a no-op, and maj@k collapses to plain sample-and-vote, no sandbox per chain.

Sampling wide is the easy half. Everything hard about fan-out is downstream of it, in whatever picks the winner, and that is a different problem depending on what came back.

7 Lean

Moves verification to an exact grade: the checker cannot be talked round.

Everything up to here is the coding harness with a maths model dropped in. Lean breaks that pattern in two places, and both are plumbing problems rather than conceptual ones. What the compiler-in-the-loop buys is in the reasoning notes; what it costs to install is here.

The first break is the executor, and it is mostly good news. The orchestrator is the solver’s loop with a different halting rule, and the sandbox is still the same run(code) -> result box — now with a Lean server where the IPython kernel sat, POSTing a candidate proof and getting back {"ok": bool, "errors": [...]}, and the errors going back into the next prompt where a tool result used to go.

A Lean toolchain plus a built Mathlib is gigabytes and hours to compile, and the prebuilt cache that skips the rebuild only matches an exactly pinned toolchain — so pin Mathlib to the model’s commit, or proofs fail for reasons that have nothing to do with the maths, because the lemma the model cites was renamed after it was trained. Underneath, the executor runs atop one of lean-repl (the lightest), Pantograph, or LeanDojo, usually behind the Kimina Lean Server so Mathlib isn’t re-imported for every proof. This lean_image business is fiddly, version-sensitive plumbing. Modal’s own theorem-proving case study shows how it is done.

The second break is at the front of the pipeline, and it has no clean fix. A prover takes a formal statement, so anything starting from an English sentence needs autoformalization first, from a separate and much less reliable model (Kimina-Autoformalizer, Goedel-Formalizer-V2). Practically: start from a formal statement, as the benchmarks do, and the prover mirrors the solver almost line for line. Start from English and the least trustworthy link in my chain is now the statement rather than the proof, which is much more annoying to debug because the failure looks like a maths failure.

8 Where the compute comes from

What the steps cost to run once built, where fan-out is the only one that costs much.

Build and debug the whole loop on a laptop first — a local IPython kernel for the solver, lean-repl on disk for the prover — and never pay for a GPU until we fan out.¹ Modal is a tidy backend to fan out to.

Tokens come from a model behind a scale-to-zero, OpenAI-compatible vllm serve endpoint — a few dozen lines mount a Volume so the weights download once, and the GPU drops to zero between requests, meaning we pay only for the seconds a request actually runs.

Fan-out is then just a .map — one chain per call, each with its own sandbox, all sharing the one endpoint:

# maj@k as a fan-out
answers = solve_one.map([problem] * 32, range(32))   # 32 chains, 32 sandboxes, one endpoint
winner  = Counter(a for a in answers if a).most_common(1)[0][0]

The same shape sweeps a whole problem set, or runs a prover’s Pass@k with the Lean verifier as the executor. A heavy tool — a Gröbner basis, a big symbolic integral, a Sage or PARI-GP call — goes on its own cheap CPU modal.Sandbox next to the GPU endpoint, so we are not paying for an idle H100 to run SymPy.

# maj@k against a local oMLX endpoint — the reasoner emits no code, so no sandbox
from openai import AsyncOpenAI
import asyncio, re
from collections import Counter

client = AsyncOpenAI(base_url="http://localhost:8000/v1", api_key="x")
BOXED  = re.compile(r"\\boxed\{([^}]*)\}")

async def sample(problem):
    r = await client.chat.completions.create(
        model="vibethinker-8bit",
        temperature=1.0, top_p=0.95,   # per request; see below
        messages=[{"role": "user", "content": problem}], max_tokens=32000)
    hits = BOXED.findall(r.choices[0].message.content or "")
    return hits[-1].strip() if hits else None   # last boxed = the final answer

async def solve(problem, k=16):
    answers = await asyncio.gather(*(sample(problem) for _ in range(k)))
    votes   = Counter(a for a in answers if a)
    return (votes.most_common(1)[0][0] if votes else None), votes

9 What the build taught me

Three things, in decreasing order of how much they surprised me.

The loop is the half I can build, and it is also the half that pays. The ablations put iterative refinement first and memory second, and both of those are a weekend of ordinary Python around models I did not train. Nothing further up the table needed a GPU either — the entire thing debugs on a laptop, and the first dollar goes on fan-out.

But the model I point the loop at cannot be chosen from a benchmark table, because responsiveness to a scaffold appears on no leaderboard. The number that matters is how the model behaves inside my loop — whether it reads a compiler error and does something different next round, whether its scratchpad note is any good. So the shortlist comes from benchmarks and the choice comes from measurement, which means budgeting for the measurement.

And most of the fiddly work was not mathematics. Deciding whether two answers are the same, pinning Mathlib to the commit the model was trained against, getting a local server to honour a temperature — that is where the days went, and none of it is the part I found interesting. The mathematics was the easy bit, which is either encouraging or ominous depending on the hour.

10 Incoming

• The Journal of Artificial Mathematics
• Bolzano (source) — a colleague’s “automatic researcher” aimed at open problems

Which chat window we read all this in is a separable and much duller problem, and has its own page.

11 References