# MathResearchOS

A recoverable, audited operating system for mathematical work. A QRS@NTU research project.

- Overview: https://qrsntu.org/projects/mathresearchos/
- Usage guide: https://qrsntu.org/projects/mathresearchos/details/

Plain-text summary for AI agents and readers, generated from the facts behind the pages; the pages are the full account.

## What it is

MathResearchOS is a zero-dependency Python runtime that turns one mathematical objective into a recoverable, audited run. Each case keeps the exact objective, a frozen contract, an executable stage graph, every attempt and an append-only event log. Stages are carried out by model backends (the Codex CLI, the Claude Code CLI, OpenAI-compatible HTTP endpoints, or a manual hand-off to a human), and every stage output passes a verifier verdict (accept, repair, replan or escalate) before the next stage uses it. RESULT.md is written only after a verifier accept.

## How to use it

- Install: Python 3.11+, `pip install -e .`, and a logged-in `codex` and/or `claude` CLI for live runs. Dry runs need none of these.
- Create a case: `mathos create --mode solve --title "..." --objective-file problem.md`; add `--workflow v2 --explorers N` for the tiered workflow with a seeded explorer swarm.
- Preview, then run: `mathos run CASE --dry-run` makes no model calls and prints the resolved model for every stage; `mathos run CASE` makes real calls.
- Choose models: `--route openai | claude | cross | cross-rev`, `--mix` (for example `claude/openai`, or per role with `role=family:model@effort`), or `--pool pool.json --route NAME`.
- Follow a run: `mathos status CASE`, `mathos events CASE --last 20`, `mathos pause CASE`, `mathos resume CASE`.
- Human gates: `mathos approve-contract CASE --accept`, then `mathos continue CASE --restart-at STAGE --reason "..." --confirm`. Models only reachable in the ChatGPT app go through `mathos handoff`.
- Larger jobs: `mathos campaign SPEC --dry-run`, then `--confirm-live`. Lean audit: `mathos lean-check FILE.lean --target THEOREM`.

## Evidence so far

- Pilot MATH-0003 (IMO-ProofBench, problem PB-Basic-008, workflow v2, 8 explorers): 17 calls, about 11 minutes. All 8 explorers delivered distinct ideas; the final proof was correct, checked by hand. 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 yet.

## Not claimed

- An accept is not a Lean kernel certificate and not a guarantee that a statement is true.
- The pilot is one problem on a public benchmark and measures no accuracy.
- No model comparison on held-out problems has been run.
- Same-family checker verdicts are provisional.
- Cost figures are list-price bounds or a CLI's reported cost, not billed amounts.

## A question to start with

Walk me through installing MathResearchOS and running my first problem, then tell me what an accepted result does and does not establish.