Jacobian

What is Jacobian about?

Jacobian is an MCP server, CLI, and Python library that equips AI agents with small, well‑defined mathematical capabilities rather than a monolithic solver. Each operation yields typed results (artifacts) that can be independently re‑checked by a trusted verifier, keeping the trust boundary explicit.

How to use Jacobian?

• Installation (Node launcher): npm install -g jacobian then run jacobian setup to register the server with supported MCP clients.
• Installation (Python): python -m pip install jacobian.
• Start the server: jacobian mcp (or npx -y jacobian mcp).
• Discover capabilities: query capability://catalog or use capability.describe.
• Invoke a capability: capability.invoke with the desired operation and arguments.
• Workspace: use workspace.open, workspace.write, and workspace.query to store agent‑authored state.

Key Features

• Runtime capability catalog with capability.describe and capability.invoke.
• Typed artifacts that include provenance, execution status, and certificates.
• Independent verification layer; only authorized checkers can emit VERIFIED records.
• Broad mathematical domains: polynomial maps, algebra, linear algebra, graph theory, SAT/SMT, universal algebra, polytopes, Lean formal verification, and research memory.
• Pluggable backends (CaDiCaL, cvc5, FLINT, Lean, Z3) with optional installation.
• Deployable MCP server via local launch, systemd, Caddy, or Tailscale Funnel.
• Versioned Python kernel managed by uv for reproducible environments.

Use Cases

• Automated conjecture testing: agents generate a claim, search for witness, and obtain a verified counterexample.
• Formal proof assistance: retrieve Lean declarations, check proofs in pinned environments, and bind certificates.
• Exact linear‑system solving: obtain rational solutions or inconsistency certificates that can be replayed.
• Graph analysis: enumerate paths, test isomorphism, and verify colorings with guaranteed artifact replay.
• SAT/SMT model generation: produce models or DRAT/Alethe proofs and independently replay them.

FAQ

Q: Do I need a separate JavaScript API? A: No. The npm package is only a launcher; all kernel functionality lives in the Python package.

Q: Which Python version is required? A: Python 3.12 (or newer) is required; the package also supports the uv tool for dependency management.

Q: How are backends handled? A: Capabilities that rely on optional backends (e.g., CaDiCaL, cvc5, FLINT, Lean) are only advertised when the corresponding tools are installed. They do not affect verification authority.

Q: Can I run Jacobian as a remote service? A: Yes. Use the provided ./deploy/install.sh script to set up a systemd service, a Caddy‑managed domain, or a Tailscale Funnel endpoint. Authentication is token‑based.

Q: What is the trust model? A: Evidence produced by search or solver code is unverified until an authorized checker replays the artifact and emits a VERIFIED record bound to the original claim.

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 upgrade
jacobian doctor

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

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

The default init output is a short onboarding summary. Add init --json when a script needs the complete reference catalog.

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

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

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:

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.

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

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

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

The lean.check capability binds an exact proposition and proof body to its result. The bundled environments pin Lean, imports, and their allowed trust bases; model-supplied imports and packages are rejected.

Prepare the pinned runtime with:

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

Proof-state interaction and premise retrieval are exploration aids. Their output cannot become VERIFIED without a successful lean.check. See the guided declaration-discovery tutorial.

The locked environment uses z3-solver 5.0.0.0. Its upstream macOS wheels target macOS 13 or newer on Apple silicon and Intel. On an older release, uv falls back to a source build that requires CMake, make, and a C++20 compiler.

Install the Xcode Command Line Tools and CMake before retrying uv sync --dev. These commands report the relevant environment without changing it:

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

See the z3-solver 5.0.0.0 files on PyPI for the upstream wheel tags.

Status

Jacobian 0.6.0 is a pre-stable release. Its published package, capability, and artifact contracts describe the current supported surface; ongoing capability research may change experimental contracts between releases.

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.

The visual motif comes from the three-dimensional counterexample to the Jacobian conjecture: an exact constant Jacobian determinant alongside three distinct rational inputs with the same output. The equations are unusually good shorthand for Jacobian's purpose—surprising candidates are valuable, but exact computation and independent checking establish what can be trusted.

Terence Tao gives an accessible mathematical account. The determinant identity and collision have also been independently formalized in Isabelle/HOL. The two-dimensional conjecture remains open.

Jacobian does not aim to put a universal mathematical ontology, a natural-language-to-formal-mathematics translator, distributed search infrastructure, or an opaque generic solver into the kernel. It does not reimplement theorem provers or SAT/MIP solvers, accept arbitrary model-supplied executable bundles, or treat floating-point scores, timeouts, and solver labels as proofs.

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