# Open Math Harness: a capability kernel for maths agents, with Lean as the only judge of a proof
> Satyajit Ghana — Head of Engineering @ Inkers Technology
> canonical: https://ai.thesatyajit.com/articles/open-math-harness
> date: 2026-10-23
> tags: formal-methods, math, agents, verifiers, multi-agent, tree-search, rust
On 23 October the SAIR Foundation [posted](https://x.com/SAIRfoundation/status/2113499940920123706) that Open Math Harness is open source: "the runtime of Open Math OS, infrastructure for Math 2.0", built for "agents on open models with math and scientific computing tools, parallel exploration in Ultramath, autoformalization in Lean". One reply asks a good question: does Ultramath keep its dead ends? (It does. Details below.)
The repository is not a Python agent script with a Lean call bolted on. It is 111,132 lines of Rust across 51 workspace crates (measured, `wc -l` over tracked `.rs` files at commit `80247afe`, 22 October), and the core is a capability-based microkernel. Its slogan is "agents propose, mathematicians decide", and the code sorts every decision into two piles: the ones Lean makes and the ones a model makes. That split is the most useful thing to know about this release.
I read the kernel and the Lean, proof-search and swarm services, built the crates that matter and ran their tests. Then I fed the repository's own `verify` function twelve candidate proofs on a real Lean 4.33.1, forgeries included.
## What the repository is
Open Math OS is the hosted product: a chat app where each team project gets a Linux VM, a choice of open-weight models, and a Lean and Mathlib install. Open Math Harness is what runs inside that VM. Its first generation is called Nucleus, and the current release is 0.41.0.
The README is honest about scope: the repository "does not yet provide a standalone local setup for interactive agents or proof search." Locally you get a scripted capability demo (it needs `bubblewrap`) and the test suites. So I did not run an agent proving a theorem. I ran the parts that decide whether a theorem was proved.
The layout follows one rule from `AGENTS.md`: mechanisms in the kernel, behaviour in services.
| Layer | What it holds |
|---|---|
| `kernel/` | process identity, capabilities, handles, IPC, lifetimes |
| `platform/` | host processes, `bubblewrap` confinement, Linux identities, cgroups |
| `interfaces/` | one versioned interface per service, shared by provider and consumers |
| `program-files/` | the programs, one binary each: `chat-agent`, `lean`, `prover`, `discovery`, `openrouter`, `shell`, `memory`, … |
| `deploy/vm/` | `nucleus.json`, the composition a team VM boots |
## Capabilities, not prompts
The kernel knows nothing about models, Lean or chat. It knows which process holds which capability: an action on a resource, with a call budget and an expiry. Authority arrives only in a spawn's grants, and delegation can only narrow it. A prover worker in proof search holds exactly three things: `model complete` on one model with a `max_calls` budget, `explore` on its own `[run, problem, task]` slot, and either `lean check` (the fixed loop) or `shell exec` plus `lean verify` (the tool loop). No network, no files outside its own directory. A "solved" claim in the model's text, say the docs, "counts for nothing".
One decision deserves copying: no request to the Lean service carries the statement being proved. The resource path names the problem, and the service looks up the frozen file it registered for that run, so a worker can only ever be judged against its own run's statement.
The prompts are adapted from OpenAI Codex, and `prompts/NOTICE` says what was not copied: Codex's guardian classifier decides command safety; here that text is "description only", and the kernel decides.
## Agents on open models
Models are reached through `nucleus-openrouter`, an OpenRouter-style chat-completions adapter pointed at `https://api.openmathmodel.org/v1`. Defaults from `deploy/vm/nucleus.json` (reported; config a team can change):
| Parameter | Default |
|---|---|
| `swarm_models` | `omm/kimi-k3`, `deepseek/deepseek-v4.1-flash`, `z-ai/glm-5.3-flash` |
| `discovery_model` | `deepseek/deepseek-v4.1-flash` |
| `discovery_reasoning_effort` | `max`, temperature 1 |
| `discovery_max_usd_per_problem` | 20 |
| `discovery_max_attempts` | 400 |
| `lean_timeout_secs` | 240 |
Only the adapter can read the API key. A request carries one project header, which the gateway uses "to keep a project that does not take part in training out of its export". That gateway is not in this repository, so I cannot check the homepage's "Training · Off" toggle.
## The tools a project gets
The best evidence of the tool set is what the composition tells the agent is installed: Lean 4 with a fully built Mathlib on `LEAN_PATH` (it says the import maps "about 6.4 GB", taking "about 2 to 3 s" warm and "about 20 s" cold, "measured with Lean 4.33.1"); Mathlib's source plus TSV declaration indexes; `python3` with `numpy` and `sympy`; CSLib; nauty and Traces; Graphviz; Plotly; TeX Live; and `scikit-fem`, `py-pde` and `meshio` for PDEs.
The homepage advertises SageMath and PARI/GP among "100+ preinstalled" tools. Neither appears in the agent's tool text. They may sit in `/opt/math/bin`, which is on `PATH`, but the VM image is not published, so I cannot tell.
There is no dedicated CAS, numerics or search tool. The agent gets a shell, files, web and PDF tools, skills and MCP servers, and everything above is a command it runs. A well-stocked image composes better than a tool per library.
## Proof search: a Dream-RSI tree over Lean files
The `discovery` service implements, in its own words, "Dream-RSI's policy-guided tree search, applied to theorem proving in Lean" (I covered [the Dream-RSI paper](/articles/dream-rsi) earlier).
A rollout is a **discovery tree** rooted at the frozen statement. The one atomic operation is `CONTINUE(v)`: resume node `v`'s workspace, generate one child, evaluate it. An **exploration policy** sees the revealed tree and returns a batch of at most `W` nodes to continue, or stops. It decides ordering, parallelism and stopping, and nothing about what gets generated. The run repeats this for up to `K1` rounds per problem.
For each node in a batch the service spawns one prover worker, confined as above. The `W` workers of a round run at once and coordinate through a per-problem **plan board**: each may publish a short research proposal and read the ones published before its own. Plans are untrusted text and vanish when their worker submits or exits.
The default task limits, from `interfaces/discovery` (reported):
| Limit | Default |
|---|---|
| width `W` | 2 |
| rounds `K1` | 12 |
| model calls per continuation | 3 |
| fan-out per node | 3 |
| model calls per problem | 8 |
The loop stops on a solve, after `K1` rounds, at a cost cap, or when nothing more can be funded or continued. The cost caps sum what workers report; the docs call them "an accounting bound on reported usage, not a kernel mechanism".
What is not here is the "dream" half of Dream-RSI: replaying finished trees to improve the policy offline. The repository ships the online tree and a slot for a policy program; improving the policy is left to whoever writes the next one.
The repository also ships a PutnamBench curriculum: 637 problem ids ordered "easiest first by static proxies", with 35 problems from 2023 to 2025 held out (measured, counting ids in `curricula/`). It claims no PutnamBench score anywhere.
## Scoring a half-finished proof
A tree search needs a scalar per node. Task-scoring protocol version 3, in `interfaces/discovery/src/scoring.rs`, scores a node only from what the Lean service reported:
| Lean's verdict | Score |
|---|---|
| complete, and `verify` accepted it | **1.0**, solved |
| complete, but `verify` rejected it | 0.9 |
| elaborates with `sorry` left (`sorries`) | 0.5 + 0.4 · C / (C + L) |
| errors | 0.05 |
| invalid (banned token, statement not reproduced) | 0.0 |
Here C is the number of **closed sub-proofs that count** and L the number of open leaves (remaining `sorry` goals). A `have` step counts as closed only if Lean accepted it without `sorry`, the rest of the proof uses it, and a fixed automation suite cannot prove it outright. That suite is fourteen tactics (`simp`, `omega`, `linarith`, `nlinarith`, `aesop` and nine more) under a 50,000-heartbeat cap, plus one `exact?` library search. So listing one-line Mathlib facts as steps earns nothing.
An open leaf is **hollow** when the theorem's own goal follows from its hypotheses plus that leaf, under the same suite. That catches "one easy step plus `sorry` for the rest" and restating the theorem as a leaf. One hollow leaf drops the node to the 0.5 base, whatever else it closed. The fraction is capped at 0.999, so a sketch can never round up to the 0.9 of a complete file.
I ran the repository's own `score` function on a few credit values (measured): C = 1, L = 1 scores 0.7; C = 3, L = 1 scores 0.8; C = 9, L = 1 scores 0.86; ten thousand closed steps with one open leaf score 0.8996; and any hollow node scores 0.5.
## Which branch to grow next
The built-in policy, `InitialPolicy` in Rust and `policies/pi0.py` as the same rule in Python, is short enough to state in full. Round one continues the root `W` times. After that, the continuable nodes (the root plus the leaves) are ordered by score descending, then depth ascending, then id. Invalid nodes are dropped. One slot is reserved first for the best **repair prospect**: an `errors` leaf with at most three errors, fewest errors first, then the one whose first error falls latest in the proof. If there is none, the slot goes to the `sorries` leaf with the most closed steps. The rest of the batch follows the ordering.
The widget's default tree is a tree after two rounds. Ordered, the continuable nodes are 4, 0, 2, 5, 3. Node 3 is invalid and drops out. Node 2 has two errors, so it is repairable and jumps the queue. With `W` = 2 the batch is 2 then 4; with `W` = 4 it is 2, 4, 0, 5. I checked both against `pi0.py` itself, fed the same tree over its line protocol (measured). Note what the reserved slot buys: a nearly-working file that scores 0.05 still gets a worker ahead of a sketch that scores 0.63. The scalar ranks; the observations beside it decide repairs.
A second policy, `pi_doubling.py`, keeps half of each batch on the `pi0` rule and spends the other half on fresh root attempts, with batches of 2, 4, 8 and then 16. Its seven unit tests pass (measured, Python 3.13).
A policy file is "model-written Python", run as a zero-capability child of the run's process. A policy that fails stops the rollout as `policy_failed`; the built-in one is never substituted, "so the journal never attributes a built-in decision to a policy program". Good rule.
## The verifier, attacked
Everything above rests on `verify`, in `program-files/lean`. It decides a solve under the PutnamBench protocol in five checks:
1. **Text rules, before any Lean runs.** No `sorry`, `native_decide`, user `axiom`, `set_option pp.*` or `debug.*`, and no word that runs code while Lean elaborates: `#eval`, `eval%` and a list of 50 more, from `macro` and `elab` to `IO` and `unsafe`. Comments and strings are blanked first, by a lexer that refuses anything it might read differently from Lean.
2. **The statement and preamble are kept.** The frozen `theorem … :=` line must appear verbatim, and the candidate must begin with the frozen preamble. Lean is then fed the *frozen* preamble itself, a separator command, and the candidate's text after its copy, so no definition the statement uses can be swapped.
3. **The file elaborates cleanly.** This is where Lean's kernel checks every declaration. `debug.skipKernelTC` is banned in step 1 for that reason.
4. **`#print axioms`** shows nothing beyond `propext`, `Classical.choice` and `Quot.sound`, and no `sorryAx`. The harness reads only what follows a per-run random marker, so the candidate cannot print a fake report.
5. **The fully elaborated type** (`set_option pp.all true in #check @thm`) is character-identical to the pristine statement's. This catches a candidate that keeps the surface text but changes what it means.
Lean is injected as a closure, so the decision logic is unit-tested without it; the real-Lean tests are opt-in and need Mathlib, which did not fit my disk budget (the Lean 4.33.1 release alone unpacks to 3.04 GB, measured from its archive listing). So I kept only the `lean` binary, its libraries and Lean core's `Init` (770 MB), and wrote a small Rust program that calls the repository's own `pristine_type` and `verify_text` with its own `bounded_lean_runner`, on a frozen file that needs no Mathlib:
```lean
def f (n : Nat) : Nat := n + n
theorem demo (n : Nat) : f n = 2 * n := by sorry
```
Then I gave it twelve candidates. Results (measured, shared 4-core cloud VM, CPU only; times from the first of two runs):
| Candidate | Stopped at | Verdict | Time |
|---|---|---|---|
| `by unfold f; omega` | — | accepted (`propext`, `Quot.sound`) | 504 ms |
| same, with `-- no sorry left here` | — | accepted | 252 ms |
| uses `Classical.byContradiction` | — | accepted (+ `Classical.choice`) | 252 ms |
| `by sorry` | text rules | `Forbidden(sorry)` | 0 ms |
| `native_decide` | text rules | `Forbidden(native_decide)` | 0 ms |
| `axiom cheat …` then `cheat n` | text rules | `Forbidden(axiom)` | 0 ms |
| `sorryAx _ false` | text rules | `Forbidden(sorry)` | 0 ms |
| `set_option debug.skipKernelTC true in` | text rules | `Forbidden(set_option debug)` | 0 ms |
| redefines `f` as `2 * n` | preamble | `PreambleMismatch` | 0 ms |
| proves `f n = n + n` instead | statement | `StatementMismatch` | 0 ms |
| `rfl` | Lean | `Elaboration` | 261 ms |
| new high-priority `HMul Nat` instance, then `rfl` | `pp.all` type | `TypeMismatch` | 306 ms |
Three accepted, nine rejected, and seven of the nine never reached Lean. A second run took 300 to 900 ms per Lean call; it is a shared VM.
The last row is the interesting one. It keeps the preamble and statement character for character, and Lean accepts its proof, because `2 * n` now means a multiplication that doubles `n`. Only check 5 sees it: the pristine type names `instMulNat`, the candidate's names `myMul`. The `sorryAx` row shows the layering from the other side: the `sorry` rule is a substring test, so it never reaches Lean, where check 4 would have caught it.
I also ran the test suites of the Lean service, its interface, the discovery interface, the kernel and the swarm interface: 148 passed, 0 failed, 6 ignored (measured, Rust 1.95.0 as pinned). The six ignored are the real-Lean tests, which need Mathlib.
Beside `verify`, the partial-proof calls (`check`, `analyze`, `complete`) run on a resident [Lean REPL](https://github.com/leanprover-community/repl) with Mathlib imported once. `complete` tries a fixed thirteen-tactic suite on each remaining `sorry`, splices the closers in, and hands the file to `verify`.
## Ultramath: parallel, and judged by a model
Ultramath is the chat-side counterpart, and its design is different in the way that matters. A session's agent starts a swarm of members: eight by default and at most sixteen, each with 100 model steps by default (up to 500), and a deadline of six hours by default (up to 24). Before a member may use any tool except reading the board, it must register a **direction**. A bounded model call, the duplicate check, decides whether that direction repeats one already on the board. Members post findings under their direction, work in their own directory under `.ultramath/`, and submit a report to the session's agent.
The rules are kept by code, not prompts (`swarm/board.rs`): one direction per member; giving one up takes a reason, which stays on the board; a first rejection lets the member try once more, and a second ends that direction. So, to answer the reply on the post: dead ends are kept. An abandoned or dead direction stays on the board, and the duplicate-check prompt says a proposal that "only retries it is the same direction". Every swarm writes a records file that outlives it.
Who decides a submission is the session's agent: a model. Its prompt tells it to "Judge it as a referee would: read those files, run what can be run, look for the gap", and to accept "only what you have checked". The module docs do not pretend otherwise: "A verdict is the session agent's model judgement: a persuasive wrong solution can be accepted by an agent that did not check it." The duplicate check carries the same caveat: "a member can try to talk the check past a near duplicate".
That is not a flaw: Ultramath is for problems with "no mechanical judge", as its prompt says. But the "checked by Lean" badge belongs to proof search and to Lean files an agent chooses to run, not to Ultramath's verdicts.
## Autoformalization: what is checked, and what is not
The post says "autoformalization in Lean". The repository has no autoformalization component. There is no service that turns an informal statement into Lean and then checks the translation. What there is:
- A chat agent can write Lean files and run `lean` on them through the shell, against the installed Mathlib. That is the product mock-up above.
- A proof-search task can supply its own statements, up to 16 per task. Before anything runs, `register` checks each one: the imports are exactly `import Mathlib`, the theorem is named after the problem, its proof is `sorry` alone, nothing in it runs code at elaboration, and one cold Lean run of the file, built as `verify` will build it, succeeds.
That makes the statement well-formed Lean that `verify` can judge. It cannot make it say what the mathematician meant. A statement that is accidentally trivial, or quietly weaker than the problem, will be "proved" with full kernel rigour.
This is the same gap I found in [openai/math](/articles/openai-math), where Comparator machine-checks the first three layers of the guarantee and the fourth, "the statement means what the paper says", is human judgment. Here the runtime enforces "agents propose"; "mathematicians decide" includes reading the statement. For contrast, see the [Thomson N=7 proof](/articles/thomson-n7-lean), a large formal proof of a new result, and [Leanstral](/articles/leanstral-formal-proofs), the opposite bet on the prover side: no tree, just the agent loop run longer.
## Sandboxing, stated honestly
`AGENTS.md` asks every module to distinguish "what is designed, implemented and tested", and the confinement docs do. The result is more nuanced than "everything is sandboxed":
- **Runtime programs** (the services, the Lean service, prover workers) run under `bubblewrap` "or not at all". Confinement fails closed. Prover workers get no network (`--worker-network off`) and one writable bind, their own directory.
- **The Lean service** has no network, read-only Mathlib and toolchain, and a writable scratch directory. Its verdict is read from output that elaborated code could write into, which is why step 1 bans every code-running word rather than trying to sandbox them.
- **Project commands are not sandboxed.** By design, a project's shell commands run as a plain process of the `projects` Linux user in the project's cgroup. The composition text tells the agent: "This is the VM itself, not a sandbox". Projects are not isolated from one another; the Unix boundary protects the runtime, not project A from project B.
- **Ultramath members** are told to keep to their own directory, "and nothing enforces it": their shell runs as the project user.
In practice that costs little: members are one team's agents on one problem. I still wish more projects wrote sentences like that down.
## What I ran
| What | Result |
|---|---|
| `cargo test` on `nucleus-lean`, `nucleus-lean-interface`, `nucleus-discovery-interface` | 84 passed, 6 ignored (need Lean + Mathlib) |
| `cargo test` on `nucleus-kernel`, `nucleus-swarm-interface` | 64 passed |
| `tools/test_pi_doubling.py` | 7 passed |
| `verify_text` on real Lean 4.33.1, core only, 12 candidates | 3 accepted, 9 rejected, as tabled |
| `pi0.py` over its line protocol on the widget's tree | batch 2, 4 at `W` = 2 |
All measured on a shared 4-core cloud VM, CPU only. Peak scratch use was 1.7 GB, mostly the build directory and the partial Lean toolchain. I did not run the slice example (no `bubblewrap` here), any agent, any model call, the REPL-backed `check`/`analyze`/`complete`, or anything that imports Mathlib.
## What holds, and what does not
What holds: proof search's verdict is Lean's, the frozen standard never travels in a request, and the five-check `verify` stopped every forgery I wrote, including one that elaborates cleanly and keeps the statement text intact. The scoring rule gives partial credit without paying for restatements or trivial steps. Authority is structural: a worker cannot reach a statement other than its own, and a policy program cannot grant itself anything.
What to keep in mind: Ultramath's verdicts and duplicate checks are model judgement, and the code says so. "Autoformalization" means agents writing Lean, with nothing checking that a statement is faithful. The full runtime does not run outside Open Math OS yet, the training opt-out lives in a gateway I cannot inspect, and the repository makes no benchmark claim to verify.
The idea worth taking, even if you never touch Open Math OS: enforce "agents propose" in a kernel, and label in the code every place where a model rather than Lean decides.