11. The Mathematical API and the agent orchestrator

In the diagram, one box is between the Research Workspace and the Research Agents: "Mathematical API and Agent Orchestrator". This box has two roles in one process:

• the Mathematical API is the only way for anything outside the build to read the knowledge graph or to ask for work. This includes a person's browser, an agent and an external tool;
• the Orchestrator changes requests for work into agent runs. It schedules the runs, enforces budgets and records everything. It changes the results into pull requests.

Both are in tamnd/math2-agent (api, mcp, orchestrator). m2 serve and m2 orchestrate serve them.

11.1 Principles

1. Read is free, write is a pull request. The API serves reads from the derived store of a release, or of main. Every write becomes a branch and a pull request against tamnd/math2. This is true for a write from a person in the workspace and for a write from an agent. The API has no other write path. Thus the audit (document 15) is the only gate, and git is the only history.
2. One surface, three encodings. The API uses HTTP+JSON for browsers and scripts, gRPC for the agents' tool calls inside the cluster, and MCP for any model client. One interface definition generates all three: api/m2.proto with HTTP annotations. Thus the three encodings cannot drift apart.
3. Every response says what it is about. It carries the release or commit that served it, the tag's content hash and the evidence summary. An agent that reasons from an API response can cite exactly what it saw.
4. The API never returns a status it did not compute. It serves the status that the build computed (document 04.7). It does not pass through any statement about truth from an external system.

11.2 The read surface

The methods are in groups by purpose. Each method is also an m2 subcommand and an MCP tool with the same name.

Resolve and fetch

Navigate

Search

Check and compute

These methods do work, but they do not write content. They return their results. The results are also cached by hash.

Propose (writes, via pull request)

People use the same propose methods from the workspace. The PR that results is attributed to the person, and the workspace is named as the tool.

11.3 Lean sessions

A proof is interactive work: try a tactic, look at the new goals, then try a different tactic. One HTTP call for each attempt with a full re-elaboration is much too slow. Thus the API gives Lean sessions:

• A session is a Lean REPL process (the community repl, or Pantograph-style goal-level access). It starts from the pinned toolchain with Mathlib and Math2 imported. The process is snapshotted after the imports. Thus a session costs milliseconds to start, not the 10 to 30 s that it takes to load Mathlib.
• A session holds a proof state tree. The calls are run_tactic(state_id, tactic) → new states | error, goal(state_id), branch(state_id) and close().
• Sessions run in the sandbox (document 08.6), with a memory cap and a timeout for each call. When a tactic times out, only its own call stops.
• Each runner has a session pool of a set size. The orchestrator charges session-seconds to the budget of the run.

The lean-lsp-mcp and Kimina-server style tools show the same interface (document 01). math2 uses its own interface because it must pin it to the release toolchain, sandbox it and meter it. Because of the MCP surface, any agent that can use MCP can prove things against math2 directly. This includes Claude Code with no math2-specific code.

11.4 The orchestrator: jobs

A job is a unit of work with a goal, a target and a budget. Jobs come from four places:

1. People, through the workspace or request_work ("formalise the statement of 7K3QX2", "find a counterexample to this").
2. Standing queues that the orchestrator computes from the graph: the frontier lists (Q6, Q7, Q12). Examples: each E3 statement with an F2 formal statement and no formal proof becomes a prove job. Each node with no explanation at L2 becomes an explain job. Each unconfirmed alignment older than 30 days becomes a align job.
3. Events: a Mathlib bump breaks bindings (→ bump jobs), a review becomes stale (→ review-assist jobs), a new arXiv batch arrives (→ extract and align jobs).
4. Campaigns: a project that a person defines, with a target set. Examples are "the undergraduate core list to F2" and "the Erdős problems in additive combinatorics to formal statements". A campaign is a topic node plus a goal predicate. Human research projects use the agents through campaigns (document 16.3).

Each job has this record:

job: j-2026-11-02-41a7
role: prove
target: 7K3QX2
goal: "binding formal[0] reaches E5"
priority: 0.73            # computed (11.5)
budget: {usd: 4.00, wall: 2h, lean_session_s: 3600, compute_cpu_s: 7200}
on_behalf_of: campaign:ug-core   # or a person, or schedule:standing-prove
requested_by: orcid:0000-0002-1825-0097
constraints: {models: [claude-opus-5-5, claude-sonnet-5-5]}   # native_decide: true permits native_decide, and type_change: true permits a bump rebind to another type hash

Priority

Priority is a score, not a decision by a person. Its formula has versions, as a prompt has:

priority = w1 · centrality(target)          # PageRank on the uses graph, so foundational nodes first
         + w2 · demand(target)              # workspace views, citations, campaign membership
         + w3 · unlock(target)              # how many frontier items this would move a level
         + w4 · tractability(target, role)  # learned: predicted success from past runs on similar targets
         − w5 · attempts(target, role)      # diminishing returns after failed attempts

unlock is the most important term. For example, 200 E1 statements use a lemma, and each one needs only that lemma. A proof of that lemma has more value than a proof of any one of the 200 statements. The closure structure in document 05.5 lets the orchestrator compute this.

Scheduling

• Jobs go into one queue for each role. The queues share fairly across campaigns, so that one project cannot use all of the budget.
• Portfolio scheduling. A hard target gets several cheap attempts with different strategies before one expensive attempt. The strategies use different models, different retrieval and different decompositions. This is the method that worked in the provers of 2025 to 2026 (document 01): many different samples, with a verifier as the filter, are better than one long attempt.
• Escalation ladder. A job starts at the cheapest configuration that has some recorded success on similar targets. If the job fails, it moves up the ladder: Haiku 5.5 or a small open prover, then Sonnet 5.5, then Opus 5.5 at higher effort, then Fable 5.1 at high or max effort. Each role has its own ladder. The run records tune the ladder (document 12.9).
• Deduplication. If the target and goal of a job match a running job, the orchestrator merges the new job into the running job. Sometimes a job's target had an attempt in the last N days with the same configuration, and the attempt failed. The orchestrator skips that job until something changes in the neighbourhood of the target.

11.5 Budgets

Money and compute are the real limits, so they are first-class:

• Global: a monthly budget, divided by role in orchestrator.yaml. People review this file each month and commit it.
• Per campaign: the owner of the campaign sets it. The global allocation is its cap.
• Per job: the priority tier sets it, and the orchestrator enforces it. Model calls carry token budgets. These are the API's task budgets where the model supports them, and hard max_tokens in all cases. The sandbox meters Lean time and compute time.
• Review capacity: money is not the only limit. Each role has a cap on PRs per week. The cap is a multiple of the review throughput for that kind of PR over the previous four weeks. Thus agents cannot go faster than the people who must check their work (document 21, Q-11).
• Stopping: a job stops at success, when the budget is used up, or when the agent reports that it is stuck and gives a reason. A stuck report with a reason is valuable output. "This statement appears false at n=7, here is the computation" is a result.

Each job records its spend: tokens in and out for each model, cached tokens, session-seconds, CPU-seconds and dollars. The weekly agent report (document 12.9) uses these records. The report shows what a formal proof costs, by area and by difficulty. At this time, the field does not publish this number.

The first version

The first version of the orchestrator is in the orchestrator package, and m2 orchestrate runs it on a directory of job files (tamnd/math2-agent#61). It has these parts and limits:

• One queue for each role. The orchestrator takes the roles in turn. In a role, it takes first the project or schedule that spent the least in the month, then the job with the highest priority. The priority is a field of the job, and the formula of the priority is not written yet.
• The monthly budget of each role and the monthly cap of each project or schedule are in orchestrator.yaml. A run gets the least of the money that is left to its job, to its role and to its project or schedule, and the orchestrator reserves that money while the run goes. The job budget is for all the runs of the job together. agent.Runner sets max_tokens before each turn so that the turn cannot cost more than the money that is left: it counts each byte of the request as one input token at the highest input price. Thus a run never goes over its budget, even when its last turn uses each token that it may use.
• A job starts on the cheapest rung of the ladder of its role with a recorded success on the role, and each failed run moves the job one rung up. A failed attempt on the same target, goal and rung in the retry time (7 days by default) makes the orchestrator skip that rung. A job with the target and the goal of a job in the queues merges into that job.
• A job ends at success, at a stuck report, when the ladder or the budget of the job is used up, or when a run cannot start. The orchestrator knows the past attempts from the run records in the store.
• Add refuses a job that names no person, project or schedule (rule P03).
• With -sandbox IMAGE, each call of lake, Lean and M2Extract in a run is a container of the image, with no network (11.7). The work tree is writable at /out, and the Lake packages of the tree are read-only at /work. m2 agent run and m2 orchestrate refuse to run with no image, unless -no-sandbox says that a person watches the run. The image m2-lean is not built yet, and the quotas for each identity are not written yet.
• The standing queues, the events, the portfolio of strategies and the cap on pull requests of each role are not written yet.

11.6 Run records

Each agent run makes a run record in the artefact store. The run id is the key. The record contains:

• the job record and the resolved configuration: role version, prompt version, model ids, tool versions, image digests;
• the full transcript: every model request and response (thinking blocks as the API returned them), every tool call and result;
• the tactic tree of every Lean session;
• the outcome: success with the diff, failure with the reason, or a partial result;
• the spend.

Run records complete the provenance chain in document 06.5. They are also the training and evaluation data that improve the agents (document 17.4). The system keeps them as document 06.6 specifies. Their summaries are public. When the output of a run was merged, the full transcript is public. When the output was not merged, the system keeps the full transcript but does not publish it. By default, math2 does not publish a failed attempt, but it uses the attempt to learn.

11.7 Security and abuse

• Read endpoints are public and have rate limits. Write endpoints need a GitHub identity, and the PR opens under that identity.
• lean_check, compute and Lean sessions run arbitrary code: Lean metaprograms can do arbitrary IO at elaboration time. Thus they run in the sandbox, with no network, a read-only toolchain and quotas for each identity. Anonymous use is permitted only for lean_check on small snippets, with a strict timeout.
• MCP tools that write have a mark that says so. The read-only MCP profile disables them. That profile is the default for third-party agent clients.
• Text from sources (paper text, MathOverflow posts) is data. It goes into agent contexts with an untrusted mark. It is never put in a system prompt, and it is never concatenated into a tool description (document 12.7).

11.8 The first version

The first version of the read surface is in the api package, and m2 serve serves it. It has these limits:

• It serves the last build of one working tree, not a release. A request for tag@release gives an error.
• get_source, history, topic and diff come with the provenance of document 06 and the topic pages of document 13. The check and compute methods, request_review and request_work come with the orchestrator.
• The one interface definition is the table of methods in the api package. The HTTP handler and the MCP server read the table. api.Proto makes api/m2.proto from it, with the HTTP annotations, and buf makes the Go code in api/m2pb from that file (tamnd/math2-agent#126). A test checks that api/m2.proto is the file that the table makes, a test checks that the code in api/m2pb agrees with the table, and a test checks that each gRPC call of the contract gives the HTTP answer. Thus the three encodings cannot drift apart. The gRPC service is m2.v1.ReadService, and each rpc gives one Response message with the result as a google.protobuf.Value, as each HTTP call gives the same JSON envelope. m2 serve -grpc ADDR serves it with the same rate limit for each IP address.
• The rate limit is a token bucket for each IP address of a peer, in memory. Behind a proxy or a CDN, the handler must read the address that the proxy sets.
• The MCP server is in the mcp package. It has the read-only profile only, with one tool for each read method, and m2 serve serves it over streamable HTTP at /mcp and over stdio. It uses the Go SDK of the Model Context Protocol.
• similar uses the embedding channel with the text of the node, and it has no judge label yet.
• The write methods propose_node, propose_edit, propose_binding and propose_alignment are in the propose package, and m2 serve -propose serves them over HTTP only (tamnd/math2-agent#54). The gRPC service and the MCP server do not have them yet, thus the MCP server keeps the read-only profile of 11.7. Each write needs the GitHub token of a person, opens the pull request under that identity, and passes the audit of the changed files before the pull request opens. The cap of 11.5 counts the pull requests of each method from their branch names, with twice the closed pull requests of a week over four weeks and a floor of 10. propose_binding adds the binding to the node file, and it does not add Lean code yet. request_review and request_work come with the orchestrator.

Markdown · Source · Edit