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):

Maths, as an automatically-verifiable problem class, is amenable to all kinds of nice tricks. A maths executor by default only ever checks a calculation, which is side-effect-free. As such, fifty attempts will not clobber each other, so we can, e.g. fan-out and try everything everywhere all at once.

These all cost different amounts of effort to build, and yield different amounts of effect. That last column is mostly not my measurement. The loop, scratchpad and fan-out rows come 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. The remaining two rows are mine. The oracle row reads across from their sweep over frontier models rather than from an ablation of anything oracle-shaped, and the Lean row is not a measurement at all — the compiler is the substrate their agent runs on, not a component they could take out and score.

I suspect that the table continues past my ability to build: the recursive, self-grading, re-formalizing orchestrators at the top of the mathematics leaderboard have enough startup money behind them that I am not going to reproduce one in a weekend. That is not an argument for buying instead, though, and the numbers do not make one either. The home-built loop comes out around five times cheaper per problem and solves about half as many: cheaper per attempt, weaker per problem, and the trade is ours to make rather than theirs.

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.

2 Easy mode

The baseline.

We need not be galaxy-brained. Claude works for maths just as well as it does code, as do most generalist models — 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”.

NB local clients are less capable at rendering equations, so I find I want to build Open WebUI to make equations easier on human eyes, but this is definitely lily-gilding.

3 Lend it an oracle

Dispatch tricky bits to specialist models.

Now, if we want a little more juice, we can squeeze it from our existing agent, using it as an orchestrator but delegating mathematics (or the checking of mathematics) to a specialist maths model. Practically, this means something like building an oracle (a solve() tool) to grind on knotty maths problems, splicing the result back into the orchestrator’s own reasoning. Oracle is meant in a strict sense: the orchestrator does not attempt the sub-problem nor does it check the answer. Rather it asks and believes with whatever confidence it is instructed to have.

Python harnesses like Smolagents or Qwen-Agent can simply call a Python function which wraps structured invocation of specialist models. For other agents (Claude-like, Goose, Codex, Gemini CLI, pi, Hermes) we can expose the solve() as a CLI tool. Either way, we wrap it with an agentskills.io SKILL.md to help the calling agent. Skill-blind agents can alternatively use an MCP server.

I whipped up mathx as an example of doing all three access paths — importable Python, CLI, MCP server — with the SKILL.md layered over the first two, 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 support in the orchestrating agent. When we own the loop, a fan-out is as simple as asyncio.gather. For tool-use agents, the async-handle pattern is probably the goods: We set up a handle-and-poll loop in 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 some MCP clients support Tasks at the protocol level; that might work too.

4 Build the loop

Sequentially iterate solutions, learning each time.

If easy mode plus an oracle aren’t enough, we can write a custom loop that specializes the generic one for mathematical needs.

What if we are trying to solve a hard problem? Intuitively, it makes sense to grind, learning from past mistakes at each attempt. Building a loop that supports this turns out to be kinda good actually. In the wild I have seen this as a two-role iterative system. A proposer writes a candidate answer or proof, and an executor runs or checks what the proposer wrote. The verdict — a compiler error, a failed numeric check — is fed into the next prompt as a minimal trace of what failed last time. 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. This is the single largest contributor to success increases in the AxProverBase ablations, and it is also where the maths usage diverges from the coding usage.

5 A scratchpad

Exploit context to record a longer narrative.

We can build more elaborate memory suited to an epic proof attempt, specifically, not just last turn, but of the whole proof journey thus far. The crude version pastes the whole transcript of past attempts into the prompt, but that bloats the context, and eventually overflows the window. The SOTA variant requires that after each attempt the proposer rewrites a running scratchpad of what it learned, pruned so it never grows without bound. In AxProverBase, that method buys around 7% more theorems at ~20% lower cost, and with lower variance than memoryless attempts and completist memory strategies.

6 Fan-out

Parallel proposals and checking.

Fan-out improves mathematical accuracy by evaluating many candidate solutions — maj@k or Pass@k, depending on our backend. 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? For problems that are just on the cusp of being solvable, this turns out to be helpful.

Sampling wide is not too crazy. The hard bit is working out if any of the answers were good.

7 Lean

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

So far we have been imagining english-language mathematical reasoning, which has ended up being kinda painful. Whacking in a proof assistant (in practice, always Lean) makes this much cleaner, at the cost of being weirder. Modal’s theorem-proving case study shows how it is done.

Here, the model emits candidate proofs in Lean, they are submitted to the Lean language server, and we get back {"ok": bool, "errors": [...]}, which tells us whether the proof landed.

A Lean toolchain can be tedious to set up, including gigabytes of “Mathlib” that takes hours to build and comprise brittle, version-sensitive plumbing. Various Lean technologies support this workflow (lean-repl (the lightest), Pantograph, or LeanDojo, usually behind the Kimina Lean Server to keep it warm).

The weirdness now, that is in the very manner we express mathematics. Lean is a formal language, guaranteeing formal proofs of formal problem statements, so obviously it needs formalization if we start with plain language problem statements — ideally autoformalization. One-shot autoformalization models (Kimina-Autoformalizer, Goedel-Formalizer-V2) suck though. This formal proving thing seems to work fine for formalized proofs, but getting the problem into such a state is unreliable and difficult to debug.

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 cloud 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 aren’t 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")
# naïve: [^}]* stops at the first }, so \boxed{\frac{1}{2}} wants a brace-counting scanner
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.

There is a second reason, and it is sharper because somebody has measured it. RL post-training buys pass@1 by spending the high-\(k\) tail — an RLVR-tuned model beats its own base at one sample and loses to it at hundreds — and hundreds is the regime fan-out lives in. Measured on a Lean prover, the SFT checkpoint often samples better than the RL checkpoint out of the same lab, purely because it stayed diverse. Standardized re-evaluation of the published gains points the same way, from a completely different direction: RL improvements are mostly modest and overfit small benchmarks, where supervised fine-tuning generalizes more consistently. So where a lab ships both, the SFT one is worth trying as a fan-out backend, and no leaderboard will suggest it: they report the single sample where the RL model wins.

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
• Mathematics and the LLM: 2026 – Coordinate Change

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

11 References