jacobian

<p align="center">
  <img src="docs/assets/jacobian-hero.jpg" width="100%" alt="An archival-style black-and-white photograph of a mathematician working at a chalkboard, with a constant Jacobian determinant and three distinct inputs mapping to one output.">
</p>

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

<p align="center">
  <strong>Executable mathematics for agents. Evidence an independent checker can replay.</strong>
</p>

<p align="center">
  An MCP server, CLI, and Python library for conjectures, counterexamples,
  exact computation, and formal proof.
</p>

<p align="center">
  <a href="https://github.com/morluto/jacobian/actions/workflows/ci.yml"><img src="https://github.com/morluto/jacobian/actions/workflows/ci.yml/badge.svg" alt="CI"></a>
  <a href="https://pypi.org/project/jacobian/"><img src="https://img.shields.io/pypi/v/jacobian" alt="PyPI"></a>
  <a href="https://www.npmjs.com/package/jacobian"><img src="https://img.shields.io/npm/v/jacobian" alt="npm"></a>
  <a href="https://pypi.org/project/jacobian/"><img src="https://img.shields.io/pypi/pyversions/jacobian" alt="Supported Python versions"></a>
  <a href="LICENSE"><img src="https://img.shields.io/github/license/morluto/jacobian" alt="MIT license"></a>
</p>

<p align="center">
  <a href="#quickstart">Quickstart</a> ·
  <a href="#how-verification-works">Verification</a> ·
  <a href="#capabilities">Capabilities</a> ·
  <a href="#documentation">Documentation</a> ·
  <a href="#contributing">Contributing</a>
</p>

Jacobian gives AI agents small, composable mathematical operations rather than
one opaque solver. An agent can construct an object, compute an invariant,
search for a witness, and submit exact evidence to a separate checker. Every
step remains visible as a typed result or artifact.

The trust boundary is deliberate: a search result, solver status, model answer,
timeout, or score is never promoted directly to `VERIFIED`. Only an
operator-authorized checker may emit a verified record, bound to the exact
claim, candidate, scope, semantics, certificate format, and checker identity.

## Quickstart

The npm launcher installs Jacobian and configures supported MCP clients. For a
one-off setup without a global install, run:

```sh
npx jacobian setup
```

For repeated use, install the launcher persistently and use its commands:

```sh
npm install -g jacobian
jacobian setup
jacobian upgrade
jacobian doctor
```

For the Python distribution, install the stable package directly with:

```sh
python -m pip install jacobian
```

The launcher supports Claude, Codex, Cursor, Gemini, and OpenCode. It requires
Node.js 18 or newer, Python 3.12, and
[`uv`](https://docs.astral.sh/uv/). Run `jacobian mcp` to start the server
directly.

<details>
<summary><strong>Install from source</strong></summary>

```sh
git clone https://github.com/morluto/jacobian.git
cd jacobian
./scripts/setup-agent --client codex --profile full-python --yes
```

This performs a locked full-Python sync and configures the selected agent to
start MCP from the absolute source and state paths with `--no-sync`. It also
records a doctor report containing the Git revision, package version, catalog
digest, and provider availability. See
[Configure an agent from a source checkout](docs/how-to/setup-agent-from-source.md)
for the `core`, `full-python`, `lean`, and `external-proof` profiles, dry-run,
repeatability, and rollback behavior.

Use `uv run jacobian --help` to inspect the CLI or `uv run jacobian-mcp` to
start the MCP adapter.

</details>

## How verification works

Jacobian separates finding evidence from deciding what that evidence proves.
Suppose an agent is testing the claim **“`F` is injective.”**

<p align="center">
  <img src="docs/assets/verification-flow.jpg" width="100%" alt="The claim that F is injective leads to a candidate collision, an exact independent check, and a verification record. Missing witnesses, timeouts, cancellation, and errors remain unknown.">
</p>

**Claim → candidate witness → independent check → verification record**

| Stage | Output | What it establishes |
| --- | --- | --- |
| Claim | `F` is injective | The statement to investigate; not yet trusted |
| Search | A candidate witness `(F, p, q)` | Inspectable evidence, not a conclusion |
| Independent check | Confirm `p ≠ q` and `F(p) − F(q) = 0` exactly | The candidate is a genuine collision |
| Record | Bind the checked collision to the original claim and checker identity | The injectivity claim is `FALSE · VERIFIED` |

> **No witness is not proof.** A failed search, timeout, cancellation, or error
> leaves the claim `UNKNOWN`.

In the introductory tutorial, the same boundary appears as:

```text
evaluate.batch   →  FALSE  · HEURISTIC
witness.find     →  exact witness artifact
witness.verify   →  FALSE  · VERIFIED
```

`FALSE · HEURISTIC` is an evaluation. `FALSE · VERIFIED` is a conclusion
backed by independently checked evidence. Follow
[Find and verify a counterexample](docs/tutorials/first-verified-result.md)
for a runnable example.

## Capabilities

Capabilities are discovered at runtime through `capability://catalog`,
described with `capability.describe`, and executed with
`capability.invoke`. The installed catalog is the source of truth because
availability can depend on local backends.

| Domain | Agent-visible outcomes |
| --- | --- |
| Polynomial maps | Evaluate maps, compute Jacobians, search for collisions, independently verify collisions |
| Polynomial algebra | Normalize typed expressions, factor univariate polynomials, verify identities, verify exact system solutions |
| Exact linear algebra | Compute determinants, rank, kernels, and integer row Hermite normal forms; find and independently verify rational solutions or inconsistency certificates for `Ax = b` |
| Graphs | Construct and inspect graphs, enumerate paths, realize degree sequences, test isomorphism, search colorings |
| SAT and SMT | Find models or proof artifacts; independently replay assignments, DRAT proofs, and Alethe proofs |
| Universal algebra | Evaluate finite magma laws and search for countermodels |
| Polytopes | Compute convex combinations and linear separations |
| Lean | Discover declarations, retrieve premises, inspect proof states, and check proofs in pinned environments |
| Research memory | Store revisioned scratch work, findings, attempts, focus, and dependency-linked context |

See the [tool reference](docs/reference/tools.md) for the public surface and
the [atomic capability portfolio](docs/contributing/atomic-capability-portfolio.md)
for portfolio design and evaluation gates.

## Design

Jacobian keeps four responsibilities separate:

- **Agents own strategy.** The kernel supplies mathematical operations, not a
  prescribed research workflow.
- **Capabilities expose one coherent outcome.** Useful intermediate objects,
  failures, and proof obligations remain visible.
- **Artifacts carry context.** Results report execution status, provenance,
  scope, completeness, exactness, assurance, and available certificates.
- **Checkers own trust.** Plugins and search code cannot authorize a checker or
  change verification policy.

The public MCP surface stays small: the capability catalog plus
`capability.describe`, `capability.invoke`, and three direct workspace tools.
`workspace.open`, `workspace.write`, and `workspace.query` manage durable
agent-authored state; workspace entries remain `UNVERIFIED`.

## Documentation

| Start here | When you need detail |
| --- | --- |
| [Documentation home](docs/index.md) | Tutorials, how-to guides, reference, and explanation |
| [Architecture](docs/explanation/architecture.md) | System shape and the independent verification boundary |
| [Product model](docs/explanation/product-blueprint.md) | Capability contracts, ownership, artifacts, and assurance |
| [Product goals](docs/explanation/goals.md) | Active priorities and research direction |
| [Tool surface](docs/reference/tools.md) | MCP resources, tools, and invocation contracts |
| [Domain operation library](docs/reference/domain-operation-library.md) | Built-in producer, bounded-search, artifact, and exact-replay contracts |
| [Provider runtime](docs/reference/provider-runtime.md) | Backend availability, compatibility, and identity |
| [v0.2 specification](docs/reference/specifications/v0.2.md) | Last frozen release snapshot and conformance baseline |
| [Testing strategy](docs/reference/testing-strategy.md) | Validation layers, commands, and CI responsibilities |
| [Capability development handoffs](docs/reference/capability-development-handoffs.md) | Evidence-preserving agent handoffs between discovery, implementation, checking, and evaluation |

Specialized contracts cover
[SAT artifacts](docs/reference/sat-artifacts.md),
[SMT/Alethe artifacts](docs/reference/smt-artifacts.md),
[exact rational linear-system evidence](docs/reference/linear-rational-solutions.md),
[exact rational matrix determinants](docs/reference/matrix-rational-determinant.md),
[integer matrix HNF](docs/reference/matrix-hermite-normal-form.md), and
[Lean declaration discovery](docs/reference/lean-declaration-discovery.md).
The [domain-capability how-to](docs/how-to/invoke-domain-capabilities.md)
demonstrates discovery, computed invocation, bounded-result interpretation,
and exact replay. The
[Lean formal-intermediates reference](docs/reference/lean-formal-intermediates.md)
covers proof states, premise retrieval, dependency graphs, and checked edits.
Architecture decisions are recorded in the
[ADR index](docs/explanation/adr/index.md).

## MCP clients and deployment

`jacobian setup` registers the local server with one or more supported clients.
`jacobian upgrade` refreshes the pinned Python kernel in the launcher's managed
environment; use `npm install -g jacobian@latest` to upgrade the npm launcher
itself.
For a clone, `jacobian setup --source <checkout> --state-dir <path> --profile
full-python` explicitly binds the client to that source environment;
the maintained `scripts/