Jacobian

Pure mathematics for agents: search for examples and counterexamples, compute exactly, and independently check what a result proves.

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.

Quickstart

For a guided user-local install:

curl -fsSL https://raw.githubusercontent.com/morluto/jacobian/main/npm/install.sh | sh

The installer resolves an npm release to an exact version, installs the small launcher without lifecycle scripts, configures selected MCP clients, and verifies the local server. The Python package environment is approximately 160 MB; if Python 3.12 is not already available, uv's managed Python adds about 110 MB. Add --defer-runtime to postpone both until first use:

curl -fsSL https://raw.githubusercontent.com/morluto/jacobian/main/npm/install.sh | \
  sh -s -- --client codex --yes --defer-runtime

For a one-off setup without a persistent launcher:

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 plus Python 3.12 or uv; the guided installer can install its pinned uv release after confirmation. Run jacobian mcp to start the server directly.

The Python distribution contains the mathematical kernel, CLI, and MCP server. The npm package is a sub-100 KB thin launcher and MCP client installer for that same implementation; it is not a separate JavaScript API. The npm tarball has no npm runtime dependencies. The larger download is the local Python mathematical runtime, not a JavaScript dependency tree.

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

A simple counterexample

Here is a small counterexample an agent can reason about directly:

Claim: every prime is odd
Agent checks: 2 is prime and even
Counterexample: 2
Conclusion: the claim is false

Here 2 is a witness: the actual example that disproves the claim. For a much larger search, Jacobian can preserve the candidate and the exact checks used to establish it.

A checked counterexample

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.

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