Jacobian

Jacobian gives AI agents reliable mathematical tools that produce evidence an independent checker can verify.

English · 简体中文

Jacobian is a collection of mathematical operations for AI agents. It runs as an MCP server and is also available as a CLI and Python library. Agents can use it to compute invariants, search for examples or counterexamples, work with solver artifacts, and check formal proofs.

The important part is that Jacobian does not treat every successful computation as a proof.

It exposes focused mathematical operations through a common interface. An agent decides which operations to use and in what order. Results stay visible as typed values or durable artifacts.

A small example

Suppose an agent is testing the claim “F is injective.”

A search returns two points, p and q, with the same image. That is a candidate counterexample, not yet a trusted conclusion.

p ≠ q
F(p) - F(q) = 0

An independent checker confirms those relations exactly. The checked collision can then be bound to the original claim and checker identity, producing FALSE · VERIFIED.

If the search finds nothing, times out, is cancelled, or fails, the claim remains UNKNOWN. Absence of a witness is not proof.

The introductory tutorial shows the same boundary in a runnable graph example.

Quickstart

For a one-off setup without a global install:

npx jacobian setup

For repeated use:

npm install -g jacobian
jacobian setup
jacobian upgrade
jacobian doctor

For the Python distribution:

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.

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.

To run the exact code in a clone, follow Configure an agent from a source checkout.

Available mathematics

The installed operations vary with local providers, but the maintained portfolio covers work in:

• polynomial maps and polynomial algebra;
• exact linear algebra;
• graphs, paths, colorings, and isomorphism;
• SAT and SMT models and proof artifacts;
• finite and universal algebra;
• polytopes; and
• Lean declaration discovery and proof checking.

Some operations require optional local backends. Catalog membership means an operation is installed and invocable; it does not grant verification authority. Read capability://catalog or use math.find to inspect the current environment. Use math.run to invoke a selected operation.

See the domain operation library for the maintained operation portfolio and optional backend setup for provider requirements.

Verification model

Jacobian separates finding evidence from deciding what that evidence proves. Search, generation, evaluation, and computation cannot certify their own conclusions.

Claim → Candidate → Independent check → Record

Only an operator-authorized checker may emit a verified record, bound to the exact claim, candidate, scope, semantics, certificate format, and checker identity. Plugins and search code cannot authorize a checker or change verification policy.

No witness is not proof. A failed search, timeout, cancellation, error, or completed bounded search without a witness leaves the claim UNKNOWN.

A formal claim may still be a poor translation of the informal conjecture. Jacobian records that correspondence and its review status; schema validation does not establish it automatically.

The architecture document describes the complete trust boundary.

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.

Documentation

• Documentation home — tutorials, how-to guides, reference, and explanations
• First verified result — a complete runnable example
• Architecture — runtime structure and trust boundaries
• Product model — capability contracts, ownership, and project boundaries
• Tool reference — MCP resources and invocation contracts
• Optional backends — provider and Lean setup
• Remote deployment — HTTP deployment and authentication

The background to the repository artwork is documented in About the hero image.

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