MathKernel gives LLMs evidence-aware mathematics via Python library and MCP server

A mathematics runtime built for LLMs

A project called MathKernel, hosted publicly on GitHub and surfaced on Hacker News's front page, describes itself as an evidence-aware, multi-engine mathematics runtime designed for language models. It ships in two forms — a Python library, mathkernel, and an MCP server, mathkernel-mcp — so ordinary applications and LLM agents can drive the same computational surface, according to the project's repository. The MCP packaging means it plugs directly into the tool-calling conventions that current LLM clients already speak.

The premise is that models are good at interpreting what a user wants mathematically and bad at carrying out the arithmetic. MathKernel divides the work accordingly: the model parses, plans and interprets, while the kernel computes and attaches claim-specific evidence to each result.

An orchestration layer, not another solver

The repository's documentation stresses that MathKernel is a typed orchestration layer rather than a single solver. A public facade owns parsing, contexts, object identity, persistence, evidence composition, resource policy and derivation tracking, while domain adapters own the actual mathematics. The feature matrix credits established engines underneath: SymPy for symbolic algebra and calculus, Z3 and Lean for reasoning and formal verification, mpmath and its interval module for certified numerics, and NumPy, SciPy, numba and CUDA kernels for performance-critical paths.

Presentation layers sit deliberately downstream. Visualization and sonification components can render evidence, the documentation notes, but producing a polished plot or audio artifact does not create stronger mathematical evidence.

Trust labels and derivation trails

Every result carries an explicit trust level, an engine tag and a derivation trail. The project treats exact computation, checked certificates, symbolic results, certified enclosures, empirical evidence and formal proofs as distinct kinds of claims, and it is explicit that exact arithmetic alone is not a formal proof. Results whose inputs trace back to approximations keep that ancestry rather than silently shedding it. Two further caveats appear in the trust model: agreement between engines is not itself a proof, and a single trust label does not replace the full evidence bundle.

The feature matrix grades each capability by its evidence ceiling. Symbolic algebra results are labeled SYMBOLIC, with approximate input ancestry able to lower that. Exact graph algorithms produce EXACT witness certificates, while NP-hard optimization results get labeled OPTIMUM, CANDIDATE, IMPOSSIBLE or UNKNOWN rather than heuristically asserting that something does not exist. Reasoning tasks — obligation planning, equivalence checks, counterexample search — come back SYMBOLIC, EXACT or FORMAL depending on which verifier supports them.

Breadth of coverage

The documented compute surface is broad: calculus and series, integral transforms with region-of-convergence obligations, complex analysis including residues and conformal maps, typed continuous probability, exact combinatorics with generating functions, finite algebra up to GF(p^m) and Smith/Hermite normal forms, exact linear algebra, arbitrary-precision integer arithmetic, and code generation to TypeScript, Python or Rust with symbolic round-trip checks. It also reaches research-grade territory — Koopman-based finite dynamics, branching Markov tensors, and a family of information-geometry and statistical-inference domains in which exact identities, numeric spectra and Monte Carlo checks are labeled and kept separate.

Why it matters

Most LLM math tooling today amounts to a Python REPL or a single computer algebra system. That works until the model needs to know how much a result deserves trust — whether a simplification hid an assumption, whether a floating-point answer is certified, whether an optimal solution is actually optimal. MathKernel's bet is that provenance is a first-class requirement for agentic mathematics: an agent that can tell a formal proof from a plausible symbolic answer can decide when to compute more, verify harder, or hedge. The design choices — claims capped by input ancestry, presentation barred from inflating evidence, nonexistence never asserted heuristically — are a notably rigorous take on what LLM-assisted mathematics could look like. Whether the trust model holds up across this many engines in practice is the open question the project will have to answer.