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 thanone opaque solver. An agent can construct an object, compute an invariant,search for a witness, and submit exact evidence to a separate checker. Everystep 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 anoperator-authorized checker may emit a verified record, bound to the exactclaim, candidate, scope, semantics, certificate format, and checker identity.
Quickstart
The npm launcher installs Jacobian and configures supported MCP clients. For aone-off setup without a global install, run:
npx jacobian setup
For repeated use, install the launcher persistently and use its commands:
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 requiresNode.js 18 or newer, Python 3.12, anduv. Run jacobian mcp to start the serverdirectly.
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 tostart MCP from the absolute source and state paths with --no-sync. It alsorecords a doctor report containing the Git revision, package version, catalogdigest, and provider availability. SeeConfigure an agent from a source checkoutfor 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 tostart 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 errorleaves 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 conclusionbacked by independently checked evidence. FollowFind and verify a counterexamplefor a runnable example.
Capabilities
Capabilities are discovered at runtime through capability://catalog,described with capability.describe, and executed withcapability.invoke. The installed catalog is the source of truth becauseavailability 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 andthe atomic capability portfoliofor portfolio design and evaluation gates.
Design
Jacobian keeps four responsibilities separate:
- Agents own strategy. The kernel supplies mathematical operations, not aprescribed 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 orchange verification policy.
The public MCP surface stays small: the capability catalog pluscapability.describe, capability.invoke, and three direct workspace tools.workspace.open, workspace.write, and workspace.query manage durableagent-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 coverSAT artifacts,SMT/Alethe artifacts,exact rational linear-system evidence,exact rational matrix determinants,integer matrix HNF, andLean declaration discovery.The domain-capability how-todemonstrates discovery, computed invocation, bounded-result interpretation,and exact replay. TheLean formal-intermediates referencecovers proof states, premise retrieval, dependency graphs, and checked edits.Architecture decisions are recorded in theADR 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 managedenvironment; use npm install -g jacobian@latest to upgrade the npm launcheritself.For a clone, jacobian setup --source <checkout> --state-dir <path> --profile full-python explicitly binds the client to that source environment;the maintained scripts/setup-agent wrapper performs the required locked syncand doctor checks first.The server advertises the capability entry points and direct workspace tools;capability.describe(query=...) searches compact installed outcomes before anagent 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 theoperating guide and capability://catalog for the complete machine inventory.Clients with prompt support can optionally request jacobian-discover orjacobian-check-evidence for protocol scaffolding.
Remote clients can connect through Streamable HTTP or SSE with bearer-tokenauthentication and subject-bound tenant state. SeeDeploy the remote MCP server. Static tokensare intended for controlled deployments, not as a hosted identity system.
From a clean clone on a systemd host, the maintained installer can deploy alocalhost 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 additionallyrequires a connected Tailscale installation. Authentication is enabled bydefault, 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
flintextra provides Python-FLINT/Arb operations for exact rationalsystems, integer matrices and lattices, polynomials, and validated numericalcomputation. Individual capabilities and independent replay support dependon the installed catalog. - Pinned Lean
COREandMATHLIBenvironments check formal certificates.
Backend availability is not verification authority. Provider output remainsunverified until the appropriate independent checker accepts its bound witnessor certificate.
Lean certificatesThe lean.check capability binds an exact proposition and proof body to itsresult. The bundled environments pin Lean, imports, and their allowed trustbases; 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. Theiroutput cannot become VERIFIED without a successful lean.check. See theguided declaration-discovery tutorial.
The locked environment uses z3-solver 5.0.0.0. Its upstream macOS wheelstarget macOS 13 or newer on Apple silicon and Intel. On an older release, uvfalls 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 thez3-solver 5.0.0.0 files on PyPIfor the upstream wheel tags.
Status
Jacobian 0.6.0 is a pre-stable release. Its published package, capability, andartifact contracts describe the current supported surface; ongoing capabilityresearch 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 sameimplementation; it is not a separate JavaScript API.
About the hero imageThe visual motif comes from the three-dimensional counterexample to theJacobian conjecture: an exact constant Jacobian determinant alongside threedistinct rational inputs with the same output. The equations are unusuallygood shorthand for Jacobian's purpose—surprising candidates are valuable, butexact computation and independent checking establish what can be trusted.
Terence Tao gives anaccessible mathematical account.The determinant identity and collision have also beenindependently formalized in Isabelle/HOL.The two-dimensional conjecture remains open.
Project boundariesJacobian does not aim to put a universal mathematical ontology, anatural-language-to-formal-mathematics translator, distributed searchinfrastructure, or an opaque generic solver into the kernel. It does notreimplement theorem provers or SAT/MIP solvers, accept arbitrarymodel-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 documentsfocused test commands, verification rules, documentation placement, andpull-request expectations.
License
MIT
