Install it, run a problem, choose models

1Install

You need Python 3.11 or newer. The package has no third-party dependencies. From a checkout of the repository:

pip install -e .
mathos --help

This registers the mathos command. python -m mathresearchos does the same thing without installing, and the examples on this page work with either. Replace mathos with python -m mathresearchos if you did not install.

For a live run you also need at least one model CLI, installed and logged in with your own account:

• codex, the Codex CLI, for the openai family.
• claude, the Claude Code CLI, for the claude family. Use both for a cross-family setup.
• Optionally an OpenAI-compatible HTTP endpoint (for example DeepSeek) with its API key in an environment variable. This is configured in a pool file; see Pools.

Creating a case, validate, status, events and every --dry-run need none of these. To check the install without any model, run the offline tests; they make no model calls:

python -m unittest discover -s tests -v
python benchmarks/run_smoke.py

2Solve one problem

A case is one objective plus everything the run produces. Put the problem statement, exactly as you want it solved, in a text file. The system stores it unchanged in OBJECTIVE.md and never rewrites it.

Create the case

The classic workflow (v1) has eight stages and a budget of 16 model calls:

mathos create --mode solve --title "First problem" --objective-file problem.md

The tiered workflow (v2) adds an explorer swarm, a separate refuter and auditors. --explorers sets the swarm size, from 2 to 32 (default 8), and the call budget becomes 16 plus the number of explorers. Use --text instead of --objective-file for a one-line statement, and --mode research for an open-ended objective.

mathos create --mode solve --workflow v2 --explorers 8 --title "First problem" --objective-file problem.md

The command prints the new case id (MATH-0001, then MATH-0002, and so on). Look at the generated cases/MATH-0001/DIC/ and EPS/INITIAL.md: that is the frozen contract the run will follow, and the moment to fix any ambiguity in the statement. Then check the case is consistent:

mathos validate MATH-0001

Preview with a dry run

A dry run resolves the stages and the model for every role, prints the call budget, and makes no model calls and no writes. Always do it before a live run. This example uses the built-in cross preset on a v2 case with four explorers:

mathos run MATH-0002 --dry-run --route cross
Dry run: MATH-0002; ready: specify
Route: cross {"reasoning": "anthropic", "worker": "anthropic", "verifier": "openai"}
  specify (thinker) -> claude-default [claude-sonnet-5-5]
  literature (worker) -> claude-default [claude-sonnet-5-5]
  explore_swarm (explorer) -> claude-default [claude-sonnet-5-5]
  falsify (thinker) -> claude-default [claude-sonnet-5-5]
  triage (orchestrator) -> claude-default [claude-sonnet-5-5]
  integrate (thinker) -> claude-default [claude-sonnet-5-5]
  refute (refuter) -> openai-default [gpt-6.1-sol]
  verify (auditor) -> openai-default [gpt-6.1-sol]
  report (writer) -> claude-default [claude-sonnet-5-5]
  verify_final (auditor) -> openai-default [gpt-6.1-sol]
Swarm: 4 explorers, 4 in parallel, needs 2 deliveries; case call budget 20
No model calls, state changes, or external writes performed

The output above is abridged. Read any WARNING lines: they name a same-family pairing or a missing API key, and are cheaper to fix now than after a run.

Run it

A live run calls real models and may incur charges on your accounts. With no model flags, a run uses the Codex CLI alone with its own configured defaults. Choose models with --route, --mix or --pool (see Presets and mixes):

mathos run MATH-0001
mathos run MATH-0001 --route cross
mathos run MATH-0001 --mix "claude/openai"
mathos run MATH-0001 --pool pool.json --route tiered-swarm

Useful limits on any run or resume: --max-nodes N stops after N stages, and --timeout-seconds S caps each model call (default 1200, that is 20 minutes). The command exits with 0 when the case is completed, ready or paused and with 2 otherwise, for example at a human gate, so a script can tell the two apart.

3What happens in a run

A run walks a fixed graph of stages in dependency order. The v1 stages are specify, literature, explore, falsify, integrate, verify, report and verify_final. The v2 stages replace explore with explore_swarm and add triage and refute: the swarm runs N explorers, each forced onto a different method family, and triage merges their ideas with exact duplicates removed. The node fails, and is retried, if fewer than half of the explorers deliver.

The audited stages (verify and verify_final) end in one of four verdicts:

• accept: the audit accepted the supplied evidence under the contract; the run moves on.
• repair: the draft goes back for a bounded repair, at most 2 repair cycles per case.
• replan or escalate: the run stops at a human gate instead of pretending success.

RESULT.md is written only after the final verifier accepts. Failed and superseded attempts stay on disk. The design and its rationale are in the repository’s docs/OS_DESIGN.md; this guide stays with usage.

4Follow, pause and resume

mathos list
mathos status MATH-0001
mathos events MATH-0001 --last 20

status shows the case state, calls used against the budget, repair cycles, every stage with its status and attempt count, the next ready stage, the last verifier verdict, and the usage totals. A fresh v2 case looks like this:

MATH-0002 — Demo v2 [solve] status=ready
Calls 0/20; repair cycles 0/2
  specify      pending    attempts=0
  literature   pending    attempts=0
  ...
Ready: specify
Usage: 0 tokens over 0 recorded call(s)

Usage totals. Every model call writes a usage.json. status adds up the tokens by backend and counts calls that reported nothing. For Claude calls it also shows the cost the CLI reports, which is notional under a subscription. Treat the totals as a report, not a bill; the budget the run enforces is on calls and repair cycles.

Pause and resume. pause asks a running case to stop after the current stage. resume continues a paused case, and also recovers an interrupted one: stages that were running return to pending, and earlier attempts and logs are kept. resume takes the same model flags as run, so pass the same --route, --mix or --pool when you resume.

mathos pause MATH-0001
mathos resume MATH-0001 --route cross

5Presets and mixes

Each stage has a role, and each role is served by a model. Three ways to assign them, from simplest to most flexible:

Family presets

Four built-in routes need no file. openai runs every role on the Codex CLI, claude on the Claude Code CLI, cross lets Claude generate and OpenAI verify, and cross-rev the reverse. The family defaults are gpt-6.1-sol for openai and claude-sonnet-5-5 for claude. The --dry-run output prints the model resolved for each role. Change a family default with the MATHOS_OPENAI_MODEL or MATHOS_CLAUDE_MODEL environment variable.

mathos run MATH-0001 --route openai
mathos run MATH-0001 --route claude
mathos run MATH-0001 --route cross
mathos run MATH-0001 --route cross-rev

Cross-family pairs matter because a checker from the same family as the author tends to share its blind spots. A verifier in the generator’s family prints a “same-family, provisional” warning; keep it, and label the result accordingly.

Mixes

--mix sets the roles yourself. A token is family[:model][@effort], where the family is claude or openai (or the name of a pool backend), the model is optional, and @effort is one of none, minimal, low, medium, high, xhigh, max or ultra; not every model accepts every level.

• --mix claude puts all roles on one family; --mix claude/openai means Claude generates and OpenAI verifies.
• The role form is a comma list: reasoning=…,worker=…,verifier=…, and for v2 also thinker, explorer, orchestrator, auditor, refuter and writer. A mix needs at least reasoning.
• explorer alone may list several backends joined by +; they are rotated by seed, which gives a mixed-family swarm.
• A mix that leaves out auditor or refuter silently reuses the verifier. Name them.

mathos run MATH-0002 --dry-run --mix "reasoning=claude,thinker=claude:claude-opus-5-5@high,explorer=claude:claude-haiku-5-5+openai:gpt-6.1-sol@low,auditor=openai:gpt-6-astra@xhigh,refuter=openai,verifier=openai"

Defaults can come from the environment instead of flags: MATHOS_ROUTE and MATHOS_MIX. The order of precedence is --mix, then --route, then MATHOS_MIX, then MATHOS_ROUTE, then the legacy Codex-only path.

Single-family presets

If you have only the Codex CLI, or only Claude Code, the selection guide gives a ready --mix string for each case: OpenAI only (section 9.1), Claude only with Sonnet as author (9.2) and Claude only with Opus as author (9.3). Every checker verdict in a single-family setup is same-family and provisional, and its dry run prints that as WARNING lines; keep them and label the result provisional. Here is the Claude-only one from section 9.2:

mathos run MATH-0002 --dry-run --mix "reasoning=claude:claude-sonnet-5-5@high,worker=claude:claude-sonnet-5-5@medium,verifier=claude:claude-fable-5-2@high,thinker=claude:claude-sonnet-5-5@high,orchestrator=claude:claude-sonnet-5-5@high,writer=claude:claude-sonnet-5-5@medium,explorer=claude:claude-haiku-5-5+claude:claude-sonnet-5-5@low,refuter=claude:claude-fable-5-2@high,auditor=claude:claude-opus-5-5@xhigh"

Model ids differ by account. Dry-run first and replace any id your CLI does not offer.

6Pools and other backends

A pool is a JSON file that names backends and routes, for when presets and mixes are not enough. Backend types are codex, claude, openai_compat (an HTTP API such as DeepSeek, without tools) and manual (a human carries the prompt; see Manual hand-off). A route maps roles to backends. API keys are read from the environment variables the pool names and are never stored or logged.

mathos run MATH-0002 --dry-run --pool examples/pool.example.json --route tiered-swarm

examples/pool.example.json is a template: verify every model id with your own account before a live run. In the same run, a backend whose key is missing shows up as a WARNING line.

7Reading the model selection guide

docs/MODEL_SELECTION_GUIDE.md says which model to try for which role, and why. Its machine-readable twin is examples/role_recommendations.json. It is a set of priors to test, not a benchmark of this system; its own opening says the only direct evidence about the harness is one pilot problem.

• Start here. One family only: go straight to section 9 and paste a mix. Both CLIs: follow the thirteen-step decision procedure in section 7.
• Evidence tags. Every claim carries a tag: [P] primary (vendor documentation), [I] independent evaluation, [S] secondary (a lead, not a fact), [M] measured in this harness, each with the date it was read.
• Roles and picks. Section 4 gives a first pick and a cheaper alternative per role; section 5 gives cross-family pairing rules; section 6 relates cost to the assurance level you want.
• Freshness. Prices, ids and rankings change. The guide lists when to re-verify; check the date at the top before relying on it.

8Human gates

A case in the awaiting_human state does not resume itself. This happens after a replan or escalate verdict, an exhausted budget, a failed stage or a contract change. The case stays as it is until you decide. status shows the cause.

1. Read status and events, and the stage’s output under runs/, and decide what is wrong.
2. If the fix needs a change to the contract or workflow (not to the objective), edit DIC/ or the workflow, then accept it explicitly. The contract is hash-checked and a run halts if it differs from what was approved:

   mathos approve-contract MATH-0001 --accept

3. Reopen from the earliest unresolved stage. This reruns that stage and everything downstream, and keeps earlier attempts archived:

   mathos continue MATH-0001 --restart-at integrate --reason "Added the missing hypothesis to the plan" --confirm

4. Run again with mathos resume MATH-0001 and your model flags.

--reason is required and is written to the event log. A material change to the objective itself should start a new case, not a continuation.

9Manual hand-off

Some models exist only in a chat app, for example GPT-6 Pro in ChatGPT. The system cannot call them, and automating the website is likely against its terms. A manual backend lets a human carry the work instead. In a pool: {"type": "manual", "model": "gpt-6-pro", "label": "ChatGPT, GPT-6 Pro"}; in a mix: manual:gpt-6-pro. The pro-audit route in the example pool uses it as the v2 auditor.

1. Run the case. When it reaches the manual stage it writes runs/<stage>-NNN/HANDOFF.md (instructions plus one self-contained message with every evidence file inlined) and stops at a human gate.
2. Show the pending hand-off, paste the message into the chat app yourself, and save the answer to a file:

   mathos handoff MATH-0002

3. Store the reply. If several hand-offs are pending, name the stage with --node:

   mathos handoff MATH-0002 --reply answer.md
   mathos handoff MATH-0002 --reply answer.md --node verify

4. Resume. The same attempt continues, with no extra call or attempt:

   mathos resume MATH-0002 --pool examples/pool.example.json --route pro-audit

The reply is hashed into handoff.json, marked unverified, and audited like any other output. A stored reply is never overwritten. Swarm explorers cannot be manual.

10Campaigns

A campaign runs several problems across several routes. Each round an orchestrator, either a frontier model or the zero-call round_robin builtin, assigns problems to routes; every assignment is an independent case, run in parallel. The orchestrator may only choose a (problem, route) pair or stop, within the budget. It cannot accept results or touch contracts.

A spec is a JSON file with a name, the problems, the routes, an optional pool and a budget. examples/campaign.example.json is a small template, and the example pool it names must have its model ids verified for your account. Preview first; it makes no model calls, creates no cases and shows the budget and the first round:

mathos campaign examples/campaign.example.json --dry-run

Only a run with --confirm-live makes real model calls, and it refuses to start without it. --max-rounds caps the rounds of this invocation.

mathos campaign examples/campaign.example.json --confirm-live --max-rounds 1

The results go to campaigns/<name>/REPORT.md, which holds a leaderboard. A campaign can stop at its own human gate; after you have dealt with the cause, clear it with a reason:

mathos campaign examples/campaign.example.json --reset-gate "Checked the failing case and fixed the route"

A completed attempt in the report means one case’s informal verifier accepted it; it is not a certificate.

11Lean check

lean-check audits a Lean 4 file and reports kernel errors, uses of sorry, the axioms a theorem depends on, and the types of the statements. You install Lean (and Mathlib if the file needs it) yourself. Give the theorem to audit with --target, repeated for several, and the Lake project root if it is not the file’s folder:

mathos lean-check Sqrt2.lean --target sqrt2_irrational
mathos lean-check Sqrt2.lean --target sqrt2_irrational --project ~/lean/MyProject --out lean-report.json

A clean report says the kernel accepted this formal statement. Whether the formal statement says what you meant is a reader’s job; the skills/lean-audit notes in the repository describe how to check it. The repository’s skills/ folder (see skills/README.md) also has procedures for formalization, search and repair. Lean is not a stage in the pipeline.

12Where data is stored

Everything is plain files. --root defaults to the current folder, and cases/, campaigns/ and experiments/ are created relative to it. That makes a run easy to inspect, back up and diff. In the repository, cases/ and campaigns/ are untracked by git, because they hold your problems and model output.

13Safety limits

• Calls are capped. Each case has a call budget (16 for v1; 16 plus the explorers for v2) and at most 2 repair cycles. A run that reaches the budget stops at a human gate.
• Dry run first. --dry-run and campaign --dry-run make no calls. A live campaign refuses to start without --confirm-live.
• The objective and contract are frozen. If either changes, the run halts. Accepted stage artifacts are hash-checked.
• No outward actions. A run does not publish anywhere, commit to GitHub, rent compute or change your objective. It writes inside its case folder.
• Narrow tools. Claude stages run with no MCP servers loaded, and only the literature stage gets web search and fetch. This also cuts the per-call overhead of a trivial Claude call from about 266k to about 10k tokens. Codex stages still load your Codex MCP servers.
• Review before trusting. File-write limits come from prompts and the Codex workspace sandbox. They are not a security boundary against a malicious executor; do not run untrusted agents on a machine with secrets.
• Keys stay out of files. Pool files name environment variables for API keys; keys are never stored or logged.
• Sensitive problems. Unpublished results sent to a hosted model leave your machine. The selection guide recommends dropping routes whose provider may train on inputs.

14Limitations and what an accept means

A verifier’s accept means its audit accepted the supplied evidence under the contract. It is not a Lean kernel certificate and not a guarantee that a statement is true. Two models agreeing, even from different families, is still an informal audit. For a result you intend to rely on, add a human read, a witness checker or the Lean kernel.

Scope

• The runtime schedules and gates; the mathematical reasoning is done by the configured models, and no result is a formal theorem because a run completed.
• With one model family, every checker verdict is same-family and provisional. Different models, tiers, efforts and fresh context reduce correlated errors without removing them.
• There is no independent exact-arithmetic or Lean checker inside a run yet; lean-check is a separate command you run on a formalization.
• Models that exist only in a chat app go through the manual hand-off, and a person carries the text.

What the evidence does not show

• The pilot (MATH-0003, IMO-ProofBench, problem PB-Basic-008) is one problem, run once, on a public benchmark that may be in training data. One problem, one run, a public benchmark: a plumbing and diversity signal, not an accuracy measurement.
• No comparison of models or roles on held-out problems has been run. The rankings in the selection guide are third-party evaluations of the models and priors to test, not measurements of this system.
• Cost figures in the guide are list-price bounds, and a Claude cost shown by status is the CLI’s notional figure; neither is a bill.
• The two family defaults were used in the MATH-0003 pilot, but other model ids in the guide and the example pool are templates to verify against your own accounts; a dry run shows the id each role resolves to.

Implementation and reproducibility

• The package is version 0.1.0, described as an experimental orchestration core.
• Stages run one node at a time, except the explorer swarm and campaign assignments, which run in parallel.
• On Windows, the Codex sandbox relies on a Codex MCP server as a file-access fallback, so Codex stages load your Codex MCP servers.
• Gemini has no backend; it is reachable only by hand. Token and dollar totals are reported after the fact and do not limit a run.

15Troubleshooting

“Claude Code CLI not found”, or a Codex stage fails at once

The CLI for that family is not installed or not on PATH, or you are not logged in. Run claude or codex once by hand, log in, then mathos resume. Use --route openai or claude if you only have one.

“Case is locked by a run”

Another run holds the case, or an earlier one crashed. Look at mathos status first. If the recorded process is gone, release the stale lock and then resume. The command refuses if the process is still alive:

mathos recover-lock MATH-0001 --confirm-stale
mathos resume MATH-0001

The run stopped and exits with code 2

The case is at a human gate. See Human gates; status and events name the cause.

“Validation failed” or a contract-changed message

Something in DIC/, EPS/INITIAL.md, WORKFLOW.json or an accepted artifact no longer matches its recorded hash. Run mathos validate to see which. If you changed the contract on purpose, use approve-contract --accept; if you changed the objective, start a new case.

A WARNING about an environment variable in a dry run

A pool backend names an API key variable that is not set (for example DEEPSEEK_API_KEY). Set it in your shell, or choose a route that does not use that backend.

“Unknown route”, “Unknown effort” or “Bad mix item”

Route names are openai, claude, cross, cross-rev or a name from your --pool file. Efforts are the eight listed in Mixes. Role names are the nine listed there. A dry run reports these before anything is spent.

“Only 3/8 explorers delivered”

The swarm needs at least half of the explorers to deliver. The stage is retried within the budget; if it keeps failing, look at the explorers’ logs under runs/, lower --explorers, or change the explorer backends.

A stage mentions looking up a solution

status prints a CONTAMINATION WARNING when a stage output mentions markers of a looked-up solution. Read that stage’s output before trusting the result.

Claude calls use far more tokens than expected

Check status usage by backend. Claude stages already run without your MCP servers, which is what keeps a trivial call near 10k tokens; if a number is far above that, look at the stage’s prompt size under runs/.

16In brief

17Sources

This page follows the MathResearchOS repository’s README.md, START.md, AGENTS.md, docs/MODEL_SELECTION_GUIDE.md (verified 2026-11-11), docs/OS_DESIGN.md (the roadmap), skills/README.md, examples/, experiments/README.md and benchmarks/README.md, and the output of mathos --help and each subcommand’s --help. The package is version 0.1.0.