Give agents a multi-engine math kernel via MCP
MathKernel is an evidence-aware multi-engine mathematics kernel exposed as an MCP server for agents to use.
What they did
MathKernel runs as an MCP server (mathkernel-mcp, stdio, 162 math_ tools). The model parses and plans, and the kernel does the computing across SymPy, Z3, Lean, mpmath and numba/CUDA. A typical session discovers capabilities, parses an expression, creates a context, then calls math_reason to solve and verify. Long sweeps go through async jobs. Every result carries a trust label and a derivation trail.
How it went
The source gives no benchmark or outcome numbers. It documents the design: trust is capped at the weakest evidence, and decimal inputs drop a result to numeric, which blocks Lean and SMT proofs.
Worth knowing
Lean 4 and Mathlib install on first server start unless MATHKERNEL_SKIP_LEAN_INSTALL=1 is set. CUDA needs the extra nvidia pip packages, otherwise it falls back to CPU.
Labels
MathKernel is an evidence-aware multi-engine mathematics kernel exposed as an MCP server for agents to use.
A typical session discovers capabilities, parses an expression, creates a context, then calls math_reason to solve and verify.
The model parses and plans, and the kernel does the computing across SymPy, Z3, Lean, mpmath and numba/CUDA.
The “Material” label failed its quality check and is not used for selection.
Details
- Agents
- custom-built or unnamed agent
- Source
- Hacker News
- Source date
- Sep 7, 2026
- Accounts
- 1
- In registry since
- Oct 12, 2026