MatyOS

The scientific method as software — a trusted substrate any AI model plugs into to do science honestly.

MatyOS lends any model — an LLM, an agent, in time a robot's model — the discipline of the scientific method: hypothesize, test, try to refute, and label what is certain versus merely likely, with every claim checkable by a small trusted kernel. The model brings the ideas; MatyOS brings the rigor.

It has three parts:

• A discovery engine — hunts for new mathematical patterns (cross-domain transfer, PSLQ closed-form detection with a significance gate, live OEIS prior-art checks), keeping only the surprising and the not-already-known.
• A trusted verifier / proof assistant — a small dependently-typed kernel in the tradition of Lean, Coq and Agda (inductive types, recursors, propositional equality, an impredicative Prop), plus a three-valued realistic logic so conjecture and certainty never get confused.
• An MCP substrate — pip install "matyos[mcp]" or install it as a Claude Code plugin, and any model can call MatyOS to verify closed forms, check OEIS, check proofs, and run the discovery loop. See docs/mcp-server.md.

Honest status. Early, but the core is real. The kernel is sound (not yet a Lean competitor — no large library); the discovery engine finds genuine closed forms but most finds are conjectures, not proofs; the model supplies the intelligence, MatyOS supplies the rigor. 338 tests. The road ahead — elaboration, tactics, a mathematics library, broader object domains — is in ROADMAP.md.

Why MatyOS?

Lean/Coq/Agda were designed for humans, decades before LLMs. MatyOS is designed from day one around two bets:

1. Soundness is sacred. Every proof — however it is produced, including by an LLM — reduces to a term checked by a tiny trusted kernel. Nothing is ever "assumed proven".
2. Uncertainty is first-class. Real mathematical work (especially an LLM's) is full of plausible-but-unproven steps. MatyOS treats this rigorously with a three-valued logic (true / false / realistic) that lives in an epistemic layer above the kernel, so conjecture and certainty never get confused. See the realistic idea.

Install

pip (recommended)

$ pip install "matyos[mcp]"     # [mcp] pulls the discovery + MCP extras
$ matyos version
$ matyos check demo.elk         # type-check a proof file
$ matyos discover               # run the v2 discovery engine

Published on PyPI: https://pypi.org/project/matyos/.

Use it inside Claude Code (MCP plugin)

MatyOS ships as a Claude Code plugin, so any model in Claude Code can call it to verify closed forms (PSLQ), check OEIS, check proofs with the trusted kernel, and run the discovery loop. Prerequisite: uv on your PATH (pip install --user uv or brew install uv).

/plugin marketplace add MatyOS-Project/MatyOS
/plugin install matyos@matyos-plugins
/mcp                            # confirm the "matyos" server is listed

The plugin launches the server with uvx --from "matyos[mcp]" matyos-mcp, which fetches MatyOS from PyPI on first run — no manual install needed. See docs/mcp-server.md.

Standalone binary

Or download the matyos binary for your platform from the Releases page and put it on your PATH — or let the installer do it for you:

:: Windows  (run from the folder containing matyos.exe / this repo)
> powershell -ExecutionPolicy Bypass -File install.ps1

# Linux / macOS
$ bash install-matyos.sh

Open a new terminal, and the matyos command is available everywhere:

$ matyos version
$ matyos check demo.elk          # type-check a proof file
$ matyos help

matyos check exits 0 when every proof in the file holds and non-zero when any proof fails, so it drops straight into CI.

Want to build from source or contribute? See CONTRIBUTING.md.

A first proof

Proofs are written in a small, readable language (.elk) and checked by the kernel. Here is arithmetic from scratch — declaring the natural numbers, defining addition, and proving n + 0 = n by induction (stdlib/arith.elk):

inductive Nat : Type :=
  | zero : Nat
  | succ : Nat -> Nat

def add (m : Nat) (n : Nat) : Nat :=
  Nat.rec (fun (_ : Nat) => Nat) n (fun (k : Nat) (ih : Nat) => succ ih) m

def cong (A : Type) (B : Type) (f : A -> B) (a : A) (b : A) (e : Eq A a b)
    : Eq B (f a) (f b) :=
  Eq.J A a (fun (x : A) (_ : Eq A a x) => Eq B (f a) (f x)) (refl B (f a)) b e

def add_zero_right (n : Nat) : Eq Nat (add n zero) n :=
  Nat.rec (fun (m : Nat) => Eq Nat (add m zero) m)
          (refl Nat zero)
          (fun (k : Nat) (ih : Eq Nat (add k zero) k) =>
              cong Nat Nat succ (add k zero) k ih)
          n

example : forall (n : Nat), Eq Nat (add n zero) n := add_zero_right

$ matyos check stdlib/arith.elk
inductive Nat : Type0  (2 constructors)
def add : (Nat -> (Nat -> Nat))
eval ... = (succ (succ (succ (succ (succ zero)))))        -- 2 + 3 = 5
def cong : (Pi (x0 : Type0), ...)
def add_zero_right : (Pi (x0 : Nat), (((Eq Nat) ((add x0) zero)) x0))
example : (Pi (x0 : Nat), (((Eq Nat) ((add x0) zero)) x0))   [QED]

Projects & the scientific method

Real work is bigger than one proof. A MatyOS project is a directory that mirrors the scientific method — assume (hypothesis/conjecture) → state (theorem) → experiment (test) → certify (proof) — and matyos check runs the whole thing and reports the honest status of every claim. Scaffold one and check it:

$ matyos new my_theory
Created project 'my_theory'.  Try:  matyos check my_theory

$ matyos check my_theory
==========================================================
 MatyOS project: my_theory
==========================================================

theory: theories/arithmetic
  definitions: Nat, add, cong
  hypotheses / conjectures (realistic):
    [CONJ] add_comm : ...commutativity of addition...
  theorems:
    [PROVEN] add_zero_right   (certified)
  tests:
    [PASS] add_2_3
    [PASS] add_0_4
----------------------------------------------------------
 Summary
   theorems   : 1 proven (1 certified, 0 conditional), 0 open
   conjectures: 1 (realistic)
   tests      : 2 passed, 0 failed, 0 ran
   status     : OK  (exit 0)
----------------------------------------------------------

The report draws a hard line between certified theorems (depend on nothing unproven) and conditional / realistic ones (rest on an open conjecture) — and that dependency is tracked transitively, so an assumption buried deep in a chain of lemmas can never launder itself into a certified result.

When a theory is complete (no open theorems, no failed checks), seal it into a single compressed, self-describing .matyos archive — a sigma of files bundling every theory, theorem, proof and test, plus a machine-readable MANIFEST.json:

$ matyos build my_theory          # refuses to seal an incomplete project
sealed -> my_theory.matyos  (1 certified, 0 conditional, 0 open)
$ matyos info my_theory.matyos    # read the manifest without re-checking

Each file type has its own black-and-white icon:

.matyos archive (Σ) · .thm theorem (∀) · .prf proof (∎) · .hyp hypothesis (∃) · .test test (✓) · .elk definitions (λ). Full details: docs/projects.md.

A worked theory, examples/projects/arithmetic, proves m + n = n + m (commutativity of addition) by induction — a real, kernel-certified theorem, built on the equality toolkit in stdlib/eq.elk (symm, trans, cong, subst). And stdlib/nat.elk proves that ℕ is a commutative semiring — associativity & commutativity of + and ×, identities 0/1, distributivity — plus ordering (≤), every law certified by induction.

Logic is just types (Curry–Howard)

Propositions are types; proofs are programs (examples/proofs/curry_howard.elk):

def id            (A : Type) (x : A) : A := x                 -- A implies A
def const         (A : Type) (B : Type) (a : A) (b : B) : A := a
def modus_ponens  (A : Type) (B : Type) (f : A -> B) (a : A) : B := f a

example : forall (A : Type), A -> A := id

The kernel rejects non-proofs: an ill-typed term like fun (A:Type)(x:A) => x x (self-application) does not type-check, so it cannot masquerade as a proof.

The realistic idea

Classical logic forces every proposition to be true or false. Real reasoning — and LLM reasoning especially — also needs "not (yet) known". MatyOS gives this a precise, textbook semantics (Kleene K3 and Łukasiewicz Ł3 three-valued logics):

The failure of excluded middle for a realistic atom is the point: an uncertain proposition is neither affirmed nor denied. Crucially, realistic lives above the trusted kernel — conjectures carry evidence/confidence and a status (conjectured → certified / refuted), and the kernel only ever certifies real proofs. This is the intended bridge between informal LLM reasoning and formal verification (see Realistic track R0–R3 in ROADMAP.md).

Architecture

matyos/             the proof assistant
├── kernel/         the TRUSTED core — small and auditable
│   ├── core        terms, normalization, definitional equality, type inference
│   ├── inductive   inductive types, recursors, iota-reduction, strict positivity
│   └── equality    propositional equality (Eq) + the J eliminator
├── frontend/       tokenizer + parser for the .elk proof language
├── logic/          three-valued ("realistic") logic
└── cli             the `matyos` command

matyos/stdlib/      standard library, written in MatyOS itself (.elk)
examples/           example proofs (.elk)
docs/               design + language reference
ROADMAP.md          the honest, phased plan toward a Lean-class system

Trust boundary: only the kernel must be trusted. The parser, the standard library, the realistic layer, and any future tactics or LLM output all ultimately produce terms that the kernel re-checks. If the kernel is sound, a term that type-checks against a proposition is a proof of it.

Documentation

• ROADMAP.md — phased plan and current status (honest about scale)
• docs/architecture.md — design and trust model
• docs/language.md — the .elk language reference
• docs/projects.md — projects, the scientific-method workflow, and the .matyos archive
• CONTRIBUTING.md — building from source, running tests
• docs/legacy-el-language.md — the project's original imperative language

License

MIT. See LICENSE.