Open Math Harness: a capability kernel for maths agents, with Lean as the only judge of a proof

On 23 October the SAIR Foundation posted 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.

expand

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.

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):

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 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):

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:

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:

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):

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 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.

expand

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, 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, a large formal proof of a new result, and Leanstral, 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

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.