SymKit

Step-by-step symbolic math for AI agents: derive, verify, and certify formulas over SymPy, with full provenance.

English | 简体中文

What is SymKit?

An MCP server that lets AI agents do exact symbolic math through conversation. Built on SymPy, it combines known formulas into new ones, records every derivation step, and verifies each result symbolically and dimensionally — instead of leaving calculations as uncheckable LLM prose.

Works for physics, engineering, chemistry, biology, economics — any domain where formulas are combined and transformed.

Core capabilities

Example — deriving the angular frequency of a simple harmonic oscillator from F = -kx and F = m·a:

1. Load the two base formulas and substitute → m·d²x/dt² = -kx
2. Solve the ODE → x(t) = A·cos(ωt + φ),  ω = √(k/m)
3. Verify by substitution: d²x/dt² = -ω²x  ✓
4. Store the result with its full derivation history

Tools

46 MCP tools across 9 categories. Most work flows through a few high-level tools; power users can drive each step individually.

Derivation sessions

A derivation is a chain of immutable, verifiable steps. Expressions are never edited in place — if something goes wrong, session_rollback to the last good state and continue, keeping the whole derivation reproducible. Every step stores its inputs, outputs, notes, assumptions, and SymPy command, persisted as JSON under the data directory.

Formula library

Formulas live in YAML files backed by a persistent SQLite FTS5 index — deterministic, offline, instant. Entries are ranked by tier:

formula_search("Navier-Stokes", domain="fluid_dynamics")
formula_get("ns_incompressible", load_into_session=True)
math("simplify", "...", session=True)
session_complete(description="Incompressible NS momentum equation")

Search covers names, aliases (Chinese works: 雷诺数 → Reynolds number), tags, domains, descriptions, and expression text. Session output lands in staging with a deterministic id and is deduplicated; promote keepers with formula_promote, inspect tiers with formula_stats, rebuild after hand-editing YAML with formula_reindex. The index (<data dir>/formulas/index.sqlite3) is a cache — deleting it is always safe. Optional external sources (source="wikidata" | "scipy" | "biomodels") degrade gracefully offline.

Lean 4 kernel certification (optional)

session_certify() re-proves eligible algebraic-equality steps of the current session (simplify / expand / factor / combine in the rational fragment) with the Lean 4 + Mathlib kernel, using ring / field_simp. Results are attached under each step's details.lean; existing verification verdicts are never modified, and unproven only means the automation could not close the goal — not that the step is wrong. A step whose input and output are identical (x = x, 0 = 0) is reported as trivial and excluded from the proven count: the kernel discharges it instantly but validates no algebra. No extra Python packages are required.

Call lean_status() first if you are unsure whether the backend is installed — it is read-only (never runs Lean, never downloads) and reports the resolved toolchain, Mathlib, and workspace paths, where each was resolved from, which layer is missing, and the exact next command. Do not probe the filesystem or run lake --version yourself: a missing directory is not evidence, and Mathlib lives under <data dir>/lean-workspace/.lake/packages/mathlib.

Setup

# One-time: install elan + Lean 4 + prebuilt Mathlib (~1–2 GB download, needs network)
symkit-lean-setup --yes

# Optionally pin a Lean version instead of stable
symkit-lean-setup --yes --toolchain v4.24.0

Configuration knobs:

• Data directory: the Lean workspace is installed to <data dir>/lean-workspace. Set SYMKIT_DATA_DIR before running the setup (and the server) to relocate it.
• Toolchain location: lake is discovered from ELAN_HOME/bin, then PATH, then ~/.elan/bin. Point ELAN_HOME at an existing elan install to reuse it — it takes precedence, so a default ~/.elan/bin/lake on PATH cannot shadow it. Certification also checks that the selected lake already owns the Lean version pinned in the workspace; otherwise it reports lean_available: false with a directing reason instead of starting a fresh toolchain download.
• Proxies: if the download stalls or fails behind a corporate proxy, export HTTP_PROXY / HTTPS_PROXY before running the setup — the elan installer does not read the Windows system proxy settings.
• Readiness check: re-running session_certify() reports lean_available: true once the toolchain and the .symkit-lean-ready stamp are in place.

Usage notes: session_certify() requires an active session, and steps that divide by a variable need an explicit assertion that the denominator is nonzero. Supply it at certify time with session_certify(assumptions={"x": {"nonzero": True}}) (or assumptions="x nonzero"), or register it beforehand with assume({"x": "nonzero"}). Without a toolchain, everything else in SymKit is unchanged.

Installation

Requirements: Python 3.10+, an MCP-compatible client (Claude Desktop, Claude Code, Cherry Studio, …), and uv or pip.

Option A — uv (recommended)

uv tool install symkit-mcp
symkit-mcp --version

uvx symkit-mcp runs the latest release on the fly without installing.

Option B — pip

pip install symkit-mcp

(pipx install symkit-mcp for an isolated environment.)

Option C — from source

git clone https://github.com/LBurny/symkit-mcp.git
cd symkit-mcp
uv sync --all-extras
uv run symkit-mcp

Data directory

Runtime data lives per-user (via platformdirs): ~/.local/share/symkit/ on Linux, %LOCALAPPDATA%\symkit on Windows, ~/Library/Application Support/symkit on macOS. Set SYMKIT_DATA_DIR to override — e.g. per project via the MCP server env block, to isolate sessions and formula libraries. Seed formulas ship read-only inside the package; user formulas from formula_add go to a writable overlay that overrides seeds by id; session-derived formulas go to <data dir>/formulas/derived/.

Connect your client

Add an mcpServers entry (Claude Desktop: claude_desktop_config.json; Cherry Studio: settings panel).

Installed on PATH (uv tool / pip / pipx):

{ "mcpServers": { "symkit": { "command": "symkit-mcp", "args": [] } } }

Without installing (uvx pulls and caches the latest release):

{ "mcpServers": { "symkit": { "command": "uvx", "args": ["symkit-mcp"] } } }

From a source checkout:

{
  "mcpServers": {
    "symkit": {
      "command": "uv",
      "args": ["run", "--no-sync", "--directory", "<local-path>",
               "python", "-m", "symkit_mcp.server"]
    }
  }
}

Windows: if the client reports "command not found", use an absolute path, e.g. "C:/Users/you/AppData/Local/uv/tools/symkit-mcp/Scripts/symkit-mcp.exe".

Architecture

src/
├── symkit/               # Core domain library (no MCP dependency)
│   ├── domain/           # Entities, derivation engine, verifier contracts
│   ├── application/      # Use cases
│   └── infrastructure/   # SymPy engine, Lean checker, persistence, adapters
└── symkit_mcp/           # MCP server layer (FastMCP) + 46 tools
formulas/                 # Seed formula library (source tree)
tests/                    # 1187 tests

Domain-driven design: the core is independent of MCP and SymPy, engines are pluggable via protocols, and formulas/sessions persist as readable YAML/JSON.

Development

uv run pytest          # full test suite
uv run ruff check src/ tests/
uv run mypy src/
uv run symkit-mcp      # dev server

Learn more

• Architecture — DDD layering and tool inventory
• SymKit Design (中文) — in-depth technical design
• Recommended system prompt — agent-side prompt for tool-driven derivations
• Roadmap — what's coming next
• Formula library fields — YAML entry format

Acknowledgments

SymKit builds on nsforge-mcp, which pioneered the neurosymbolic formula-derivation approach, and can be used alongside sympy-mcp, a general-purpose SymPy MCP service.

License

Apache 2.0.