QRS research · Mathematical research tooling
A recoverable, audited operating system for mathematical work
Give it a mathematical objective. Get back a result with its evidence, or the exact stage where it stopped.
MathResearchOS is a command-line runtime that turns one objective into a staged run: normalise the problem, search the literature, explore proof ideas, try to refute them, integrate an argument and write it up. Models from the Codex CLI, the Claude Code CLI or an HTTP API do the work; every stage output must pass a verifier verdict before the next stage uses it. Each case keeps the exact objective, its frozen contract, every attempt and an event log, so a run can be paused, resumed or audited later.
RESULT.md is published only after the final verifier accepts.
One run of the v2 workflow, from specify to RESULT.md. A verifier verdict (accept, repair, replan or escalate) gates each audited stage; RESULT.md is published only after the final verifier accepts.
Illustrative run; stage names are the workflow’s own, verdicts vary.
Quick start
Install, create a case from a problem file, preview the run for free, then run it. The full guide covers each step.
pip install -e .
mathos create --mode solve --title "First problem" --objective-file problem.md
mathos run MATH-0001 --dry-run
mathos run MATH-0001 --route cross
mathos status MATH-0001Live runs call real models and can cost money; --dry-run never does. A live run needs a logged-in codex or claude CLI. Install details →
Evidence so far
One public-benchmark problem (IMO-ProofBench, problem PB-Basic-008) through the v2 workflow with 8 explorers: 17 calls, about 11 minutes. All explorers delivered distinct ideas and the final proof was correct, checked by hand.
One problem, one run: a check that the pipeline works end to end, not a measure of accuracy.
Model and role comparisons on held-out problems, with every arm and failure reported, are planned but not run yet.
What an accept means, and the limitations →