Maths and proof models, applied

1 The path through

Start from the coding harness I already run I can add various types of sophistication.

• Easy mode — use an agent with a generalist backend but be smart about how I use it (basic agentic)
• Lend it an oracle — keep that same agent, but give it a maths model behind a solve() tool for the sub-problems it should not attempt. (agentic + oracle)
• Custom loop — explicitly make the loop into generate-run-verify loop system and using potnetially specialist through it freely; the bare model under it is a plain solver or, for theorems, a plain prover. (our own self-correcting loop)
• Memory — Augment iterations with memory of what failed across prior attempts so the loop stops repeating itself.
• Fan-out is a trick to run multiple agents to sample solutions and cross-check, trading compute for accuracy.
• Lean formalises the problem into machine-checkable form.
• The frontier — all of the above. A self-grading, decomposing, re-formalizing orchestrator. (recursive decomposition)

That sequence is also roughly the field’s own trajectory.

2 Easy mode

An ordinary agent harness I already use for code, pointed at a good generalist reasoning model, gets me a long 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. However local clients are less capable at rendering equations, so we may want to build Open WebUI to make equations kind to human eyes.

3 Lend an agent an oracle

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.

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 depends on the arhcestrating 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 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

If easy mode with an oracle aren’t enough, we can write a custom agentic loop to specialize the generic agent loop for mathematical needs.

Recall agentic harnesses have three parts.

Model server

emits tokens — a local server, or a hosted endpoint.

Executor / verifier

acts on the model’s output — a Python sandbox that runs a code block, or a Lean compiler that accepts or rejects a proof.

Orchestrator (the loop)

generate candidate answers, run-or-compile, splice the result back, repeat. It only ever calls run(input) -> result and does not care where run happens, so we can route a calculation to a remote executor when it pays to.

That is the same skeleton as the coding harness — so what does maths add? The difference is what the executor is for. A coding executor does work: it runs the program, edits the file, prints something the model reads to pick its next move, and the loop closes when the task is done. A maths executor passes judgement: it tells us whether the candidate answer is correct. Its output is a verdict rather than a product.

Verifications loops have some nice properties; for examples, they let us spend compute to buy correctness. Generate a hundred candidate answers, let the verdict sort them, and we have fan-out. Carry a record of which verdicts came back wrong, and why, and we have memory. How far we can push this depends on how valuable is the verification in the verdict.

For a plain generalist the executor is whatever the agent’s own tools call invokes; there is no maths-specific check, so the loop trusts the model’s own say-so, give or take a vote. For a solver it is a Python sandbox running tool-integrated reasoning — emit a Python block, run it, splice the output back, repeat to a boxed answer — which catches the arithmetic and algebra slips the model cannot check in its head, though nothing certifies the final answer. For a prover it is the Lean compiler, and the verdict is exact: a proof typechecks or it does not, and a plausible-but-wrong proof still fails. That last verifier cannot be talked round, which is why the prover loops downstream can afford to sample so wide. What the executor does — and how much its verdict is worth — is the one knob the three families turn.

Two maths-harness gotchas:

• (some) Specialist models speak their own tool-call dialect, specifically TIR type. These produce fenced code templates, not the native tools/tool_calls protocol — so the orchestrator needs matching parsing.
• The model writes the code we run unobserved, sandboxing is wise. The only maths-specific detail is that the specialists assume a full scientific Python (SymPy, NumPy), build accordingly.

5 Memory

A loop that forgets repeats itself. The orchestrator splices each compiler result back within a run, but the next independent attempt starts cold — re-importing the same non-existent lemma, mis-naming the same tactic the last twenty attempts did, spending the iteration budget on mistakes already made. We can carry a record of what failed into the next attempt.

Requena et al. (2026) rank this the second-largest lever in the whole architecture — behind iterative refinement, ahead of the search tools — and it is cheap to add. 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 their numbers that buys around 7% more theorems at ~20% lower cost, with half the run-to-run variance.

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 rather than for rediscovering that Nat.foo was renamed three Mathlib versions ago.

6 Fan-out

Fan-out improves mathematical accuracy by evaluating many candidate solutions. For solvers that means maj@k, i.e. majority voting. For provers it’s Pass@k — keep any candidate that compiles. Either way we can run a lot of these fuckers at once, since the tokens stream over the network in parallel. Which sample to trust is its own question — a plain majority vote, or richer schemes that rank candidates with a verifier or let the model grade its own — but the lever is the same.

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.

# 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]

# 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:solve",          # temp 1.0 / top-p 0.95 set on the endpoint (greedy = nothing to vote on)
        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

7 Lean etc

Provers have their own requirements — the Lean-emitting family. Lean is the proof-assistant language they target, and the compiler-in-the-loop is what makes a prover a prover: everything above this works on a boxed answer, while a prover produces a machine-checked proof. Everything so far is the coding harness with a maths model dropped in; Lean breaks that pattern in two places.

The first is the executor. It stops being a Python sandbox whose output we splice back, and becomes an exact verifier: the Lean compiler accepts or rejects a proof, and there’s no arguing with it. That’s mostly good news. The compile-and-retry loop feeds compiler errors back where a tool result used to go, and stops when the compiler accepts the proof. 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:

# verifier sandbox — same interface as the IPython one, Lean underneath
@app.cls(image=lean_image, cpu=8.0, memory=32768, scaledown_window=120)
class LeanVerifier:
    @modal.method()
    def run(self, proof: str, timeout=300):
        ...   # POST to the in-image kimina-lean-server; return {"ok": bool, "errors": [...]}

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. Underneath this 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, unlike a solver, takes a formal Lean statement, so a “prove this English sentence” pipeline first needs autoformalization — a model to turn the English into a Lean theorem … := by sorry. That step is a separate, much less reliable model (Kimina-Autoformalizer, Goedel-Formalizer-V2): the formalizers produce a faithful statement only 55–75% of the time, while the verifier downstream is exact. So in a fully automated prover the weak link is no longer the proof but the statement. Start from a formal statement, as the benchmarks do, and the prover mirrors the solver almost line for line; start from English, and autoformalization is the least trustworthy link in the chain.

8 The frontier

The top of the leaderboard isn’t a bigger prover we can rent by the token. The current leaders — Aleph from Logical Intelligence, Seed-Prover 1.5, Aristotle — are API-or-pilot-only, priced in dollars per problem rather than a flat per-token rate — Aleph’s runs cost an estimated $23–$68 each. The strongest of these have cleared gold-medal-equivalent on IMO 2025 in machine-checked Lean.⁴ The open-weight specialist provers we can download — DeepSeek-Prover, Goedel-Prover — are near the bottom of that same leaderboard.

It turns out much of that performance gap, can be made up by using available models cleverly. Against the leaders much of what we lack turns out to be the right loop, not the model — we can rent a generalist nearly as good as their specialists if we use it right. Requena et al. (2026) rank iterative refinement first and memory second as features of such a loop. So the leaders are closed as products; but we might imagine that we can recover a good approximation of them from open recipes.

AxProverBase is such a harness, in the lean4 prove style. It has no recursive decomposition, and was tested with an off-the-rack Claude Opus 4.5 (no fine-tuning) in an iterative compile-and-retry loop with memory and Mathlib search. It reaches 54.7% on PutnamBench — near-parity with the open specialist Hilbert while spending about 100× fewer tokens, at roughly $12.6 a problem against Aleph’s $23–68.

The top rung is (probably) the same loop with heavier engineering, every crude part swapped for a subtler one: a self-grading model where the majority vote used to be, an interleaved formalize-and-critique step where the bare compiler used to be, and autoformalization pulled inside the loop lemma by lemma to soften the brittleness of the Lean interface.

9 Frontends

The frontend is the loosest-coupled part of the stack — the maths model neither knows nor cares what renders its tokens — so picking one is cheap and reversible. Four questions decide it:

1. Does it render maths?
2. Will it take a PDF?
3. Can it call the oracle?
4. If we are proving: can we inspect the Lean proof state?

When a hosted general agent is the orchestrator there is not much to decide: we read the output in whatever client we already drive, and the oracle hands back a short answer and a vote tally rather than a reasoning trace, so there is little to render anyway. The questions bite when we move onto open models, or build our own loop.

The Anthropic bundle takes the first two questions by brute convenience; the standard caveats about proprietary vendors apply. Among the self-hosted options, Open WebUI and Qwen-Agent are the two that answer yes to the first three.

10 See also

• The Journal of Artificial Mathematics
• AxProverBase — the reference implementation of Requena et al. (2026): the same compile-and-retry loop, plus a memory module, Mathlib search, and a two-stage review — deterministic checks for sorry/admit, then an LLM reviewer that confirms the statement wasn’t weakened and flags metaprogramming dodges that compile without proving the theorem.
• Bolzano (source) — a colleague’s “automatic researcher” aimed at open problems

11 References