Jacobian: an MCP server, CLI, and Python library that gives AI agents a composable toolbox of mathematical capabilities with inspectable artifacts and independent verification.
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.
The npm launcher installs Jacobian and configures supported MCP clients:
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.
Use uv run jacobian --help to inspect the CLI or uv run jacobian-mcp to start the MCP adapter.
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 Conf
From the project README.
Add the radar badge to your README — it shows your project was picked up by MCP Radar and links to this page:
[](https://mcp.liqiwa.com/s/morluto--jacobian.html)
A native desktop IDE for Lean 4 on macOS, Windows and Linux. Every proof re-checked by Tenet, an independent Lean 4 kernel. An MCP server for AI assistants, with Git and GitHub built in.
1105216375-alt/resimindNeuro-symbolic agents with verified memory. MCP math tools, an algebra repair Skill, and an open challenge. Verify solutions, learn checked rules, and reuse.
2akouwu/reverifyStop your AI from making things up — it proposes, deterministic tools decide, every claim checked against ground truth with evidence. Grounded facts and context survive resets. Reverse engineering is
Stupidoodle/swissdevjobs-cliSearch & apply to ~4,700 salary-transparent tech jobs across 7 countries (🇨🇭🇩🇪🇬🇧🇺🇸🇨🇦🇳🇱🇫🇷) from your terminal or AI agent — zero-dependency Python CLI + MCP server + Claude Code plugin
sepehr071/awesome-iran-mcp19 open-source MCP servers (308 tools) that give AI agents the Iranian web: Digikala, Snappfood, Jabama, MrBilit, Paziresh24, Taaghche and more. Prices in Toman.
TedHaley/pensieveLocal search across your files, git repos and AI agent sessions on your Mac. An MCP server gives your agents the best context, a 3D map shows your work by topic, and git blame shows who knows what.
The top new MCP servers of the week, every Monday. No spam, unsubscribe anytime.