Metadata-Version: 2.4
Name: matyos
Version: 0.31.0
Summary: MatyOS — a dependently-typed, LLM-native proof assistant with a discovery engine
Author: AHMED HAFDI
Author-email: Ahmed Hafdi <58536023+HAFDIAHMED@users.noreply.github.com>
Maintainer-email: Ahmed Hafdi <58536023+HAFDIAHMED@users.noreply.github.com>
License: MIT License
        
        Copyright (c) 2025 MatyOS Project
        
        Permission is hereby granted, free of charge, to any person obtaining a copy
        of this software and associated documentation files (the "Software"), to deal
        in the Software without restriction, including without limitation the rights
        to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
        copies of the Software, and to permit persons to whom the Software is
        furnished to do so, subject to the following conditions:
        
        The above copyright notice and this permission notice shall be included in all
        copies or substantial portions of the Software.
        
        THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
        IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
        FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
        AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
        LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
        OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
        SOFTWARE.
        
Project-URL: Homepage, https://github.com/MatyOS-Project/MatyOS
Project-URL: Documentation, https://github.com/MatyOS-Project/MatyOS/tree/main/docs
Project-URL: Repository, https://github.com/MatyOS-Project/MatyOS
Project-URL: Bug Tracker, https://github.com/MatyOS-Project/MatyOS/issues
Keywords: proof-assistant,dependent-types,theorem-prover,mathematics,discovery,mcp,llm
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Science/Research
Classifier: Intended Audience :: Developers
Classifier: License :: OSI Approved :: MIT License
Classifier: Operating System :: OS Independent
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.8
Classifier: Programming Language :: Python :: 3.9
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Topic :: Scientific/Engineering :: Mathematics
Classifier: Topic :: Software Development :: Libraries :: Python Modules
Requires-Python: >=3.8
Description-Content-Type: text/markdown
License-File: LICENSE
Provides-Extra: dev
Requires-Dist: pytest>=6.0; extra == "dev"
Requires-Dist: pytest-cov>=2.0; extra == "dev"
Requires-Dist: black>=22.0; extra == "dev"
Requires-Dist: flake8>=4.0; extra == "dev"
Requires-Dist: mypy>=0.950; extra == "dev"
Requires-Dist: pre-commit>=2.0; extra == "dev"
Requires-Dist: isort>=5.0; extra == "dev"
Provides-Extra: docs
Requires-Dist: sphinx>=4.0; extra == "docs"
Requires-Dist: sphinx-rtd-theme>=1.0; extra == "docs"
Requires-Dist: myst-parser>=0.17; extra == "docs"
Requires-Dist: sphinx-copybutton>=0.5; extra == "docs"
Provides-Extra: test
Requires-Dist: pytest>=6.0; extra == "test"
Requires-Dist: pytest-cov>=2.0; extra == "test"
Requires-Dist: coverage>=6.0; extra == "test"
Provides-Extra: discovery
Requires-Dist: mpmath>=1.3; extra == "discovery"
Provides-Extra: mcp
Requires-Dist: mpmath>=1.3; extra == "mcp"
Requires-Dist: mcp>=1.0; extra == "mcp"
Dynamic: author
Dynamic: license-file
Dynamic: requires-python

<p align="center">
  <img src="assets/logo.png" width="140" alt="MatyOS logo"/>
</p>

<h1 align="center">MatyOS</h1>

<p align="center">
  <strong>The scientific method as software — a trusted substrate any AI model plugs into to do science honestly.</strong>
</p>

<p align="center">
  <img src="https://img.shields.io/badge/tests-338%20passing-brightgreen" alt="tests"/>
  <img src="https://img.shields.io/badge/platforms-win%20%C2%B7%20linux%20%C2%B7%20macos-blue" alt="platforms"/>
  <img src="https://img.shields.io/badge/license-MIT-green" alt="license"/>
  <img src="https://img.shields.io/badge/PyPI-matyos-blue" alt="PyPI"/>
  <img src="https://img.shields.io/badge/status-early%20%C2%B7%20sound%20kernel-orange" alt="status"/>
</p>

---

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](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](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](#the-realistic-idea).

## Install

### pip (recommended)

```console
$ 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`](https://docs.astral.sh/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](docs/mcp-server.md).

### Standalone binary

Or download the `matyos` binary for your platform from the
[**Releases**](https://github.com/MatyOS-Project/MatyOS/releases) page and put it
on your `PATH` — or let the installer do it for you:

```console
:: 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:

```console
$ 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](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`](matyos/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
```

```console
$ 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:

```console
$ 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`:

```console
$ 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 file icons](assets/icons/contact_sheet.png)

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

A worked theory, [`examples/projects/arithmetic`](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`](matyos/stdlib/eq.elk) (`symm`, `trans`, `cong`, `subst`). And
[`stdlib/nat.elk`](matyos/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`](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):

| formula | classical | with a `realistic` atom |
|---|---|---|
| `P \/ ~P`  (excluded middle) | valid | **not valid** — undetermined when `P` is `realistic` |
| `~(P /\ ~P)`  (non-contradiction) | valid | **not valid** |
| `P -> P`  (self-implication) | valid | not valid in Kleene · valid in Łukasiewicz |

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

## License

MIT. See [LICENSE](LICENSE).
