Jacobian

Executable mathematics for agents. Evidence an independent checker can replay.

An MCP server, CLI, and Python library for conjectures, counterexamples, exact computation, and formal proof.

Quickstart · Verification · Capabilities · Documentation · Contributing

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:

npm install -g jacobian
jacobian setup
jacobian doctor

The launcher supports Claude, Codex, Cursor, Gemini, and OpenCode. It requires Node.js 18 or newer, Python 3.12, and uv. Run jacobian mcp to start the server directly.

git clone https://github.com/morluto/jacobian.git
cd jacobian
uv sync --dev
uv run jacobian --state-dir .jacobian init

How verification works

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

Claim → candidate witness → independent check → verification record

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:

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 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.

See the tool reference for the public surface and the atomic capability portfolio 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

Specialized contracts cover SAT artifacts, SMT/Alethe artifacts, exact rational linear-system evidence, exact rational matrix determinants, integer matrix HNF, and Lean declaration discovery. The domain-capability how-to demonstrates discovery, computed invocation, bounded-result interpretation, and exact replay. The Lean formal-intermediates reference covers proof states, premise retrieval, dependency graphs, and checked edits. Architecture decisions are recorded in the ADR index.

MCP clients and deployment

jacobian setup registers the local server with one or more supported clients. The server advertises the capability entry points and direct workspace tools; capability.describe(query=...) searches compact installed outcomes before an agent inspects an exact contract and invokes it. This is a toolbox interface: agents own mathematical decomposition, exploration, and composition.

Clients with MCP resource support can read jacobian://instructions for the operating guide and capability://catalog for the complete machine inventory. Clients with prompt support can optionally request jacobian-discover or jacobian-check-evidence for protocol scaffolding.

Remote clients can connect through Streamable HTTP or SSE with bearer-token authentication and subject-bound tenant state. See Deploy the remote MCP server. Static tokens are intended for controlled deployments, not as a hosted identity system.

From a clean clone on a systemd host, the maintained installer can deploy a localhost endpoint, a Caddy-managed public domain, or Tailscale Funnel:

sudo ./deploy/install.sh
sudo ./deploy/install.sh --mode domain --domain math.example.org
sudo ./deploy/install.sh --mode tailscale

Run ./deploy/install.sh --help or add --dry-run to inspect the plan first. The public modes require a reviewed Caddy installation; Funnel additionally requires a connected Tailscale installation. Authentication is enabled by default, and a newly generated bearer token is printed once.

Optional backends

Some capabilities use backends that are not installed by default:

• CaDiCaL finds SAT models and UNSAT proof artifacts.
• cvc5 produces SMT UNSAT proofs; Carcara independently checks Alethe.
• The flint extra provides Python-FLINT/Arb operations for exact rational systems, integer matrices and lattices, polynomials, and validated numerical computation. Individual capabilities and independent replay support depend on the installed catalog.
• Pinned Lean CORE and MATHLIB environments check formal certificates.

Backend availability is not verification authority. Provider output remains unverified until the appropriate independent checker accepts its bound witness or certificate.

elan toolchain install leanprover/lean4:v4.31.0
cd lean
lake update
lake build

sw_vers -productVersion
uname -m
xcode-select -p
clang++ --version
cmake --version
make --version

Status

Jacobian is pre-stable. Experimental contracts may change between releases; release specifications describe supported snapshots, not the order of ongoing capability research.

The Python distribution contains the mathematical kernel, CLI, and MCP server. The npm package is a thin launcher and MCP client installer for that same implementation; it is not a separate JavaScript API.

Contributing

Jacobian uses Python 3.12, uv, and a small Makefile:

make setup
make test-unit
make check

Read CONTRIBUTING.md before changing code. It documents focused test commands, verification rules, documentation placement, and pull-request expectations.

License

MIT