The Mathematical Claim Engine is a local-first mathematical knowledge-production and verification system built by MnehmosAI.
The binding product and implementation contract is SPEC.md. When this README, prior code, or an implementation assumption conflicts with that specification, the specification wins.
MathOS 1.0.0 is not complete or released.
The repository currently contains two bodies of work:
- A legacy Python finite-domain claim kernel. It preserves useful experiments in claim identity, verifier-gated state, provenance, CLI, MCP, and trajectory validation. It is not the specified product and carries no 1.0 release claim.
- The in-progress Rust modular monolith named
mcl, which is the canonical implementation required by the specification.
No remote v1.0.0 tag exists. Release is prohibited until the complete Definition of Done in section 30 of the specification passes and mcl acceptance --all --clean produces a verified release candidate.
MnehmosAI is the company. The Mathematical Claim Engine, exposed as MathOS, is the product.
Earlier proof-search episodes, claim records, MathCorpus packets, and MCIP bundles are migration inputs or export formats. They are not parallel applications. Their useful capabilities and histories must be absorbed without silently promoting trust.
The product contains one canonical service layer shared by:
- the
mclcommand-line interface; - the Model Context Protocol adapter;
- the local SQLite store;
- the content-addressed artifact store;
- the Lean 4 verifier worker;
- release, pedagogy, migration, and learning-export modules.
See:
- Implementation status
- Real blockers
- Release checklist
- MathCorpus and MCIP export
- RL and evaluation export
- Architecture decisions
The implementation agent must continue until the complete specification passes. A pilot, demo, schema, or partially working command is not completion.
The repository is source-available under the PolyForm Noncommercial License 1.0.0. Commercial use requires a separate license from MnehmosAI.