Open Math Harness 0.41.0 (Nucleus)

Open Math Harness is the open-source runtime of Open Math OS, infrastructure for Math 2.0. This is its first public release, from Nucleus, the runtime's first generation.

Built for everyday math research

• Agents on open models. Every chat has an agent on the open-weight model and the reasoning depth chosen for the task, with math and scientific computing tools, the shell, web and PDF tools, sub-agents and persistent session history.
• Ultramath. Several agents explore different approaches to one hard problem in parallel, share lemmas, counterexamples and dead ends, and bring their findings back to the chat for review.
• Autoformalization and proof search in Lean. Agents formalize arguments in Lean with Mathlib, and proof search runs confined prover agents on many branches of a fixed Lean statement. Whether a proof holds is decided by Lean, never by what a model says about it.
• Skills, MCP servers and plugins. Projects are git repositories. Agents use the project's skills, connect to MCP servers, and build plugins of their own.
• Project memory. Each project keeps a memory across sessions.
• People in charge. Every program, agents included, holds only the capabilities its composition grants it. A protected action waits for a person's approval, and credentials never reach a model, a transcript or a log.

Status

The full runtime currently relies on the Open Math OS deployment environment. This release supports building the runtime and running a small self-contained example on Linux with bubblewrap; it does not yet provide a standalone local setup for interactive agents or proof search. See the README for build instructions.

To use the full runtime with your collaborators, apply for a team on Open Math OS.

Community

Join the Open-Math-Model channel on the SAIR Foundation Zulip. Contributions are welcome; see CONTRIBUTING.md.

Licensed under the Apache License 2.0.