dk Dark Knight 2026-09-07 POST_READ_TIME

MathKernel MCP Teardown: The Trust Model Under Fire

MathKernel hit Show HN at 00:21 UTC today with a pitch aimed straight at the agent-tools crowd: an "evidence-aware multi-engine mathematics kernel" that gives every mathematical result an explicit trust level, an engine tag, and a derivation trail — as a Python library and a 168-tool MCP server. The HN reception was one raised eyebrow: "it has all the signs of being AI-generated... a game engine without a game." That's a lazy reason to dismiss it. The real question is whether the trust machinery does what it claims under fire. So I installed it, attacked it with false identities and catastrophic cancellation, and read the source where the labels get assigned. The verdicts held on every adversarial case I threw. What I found instead were two cracks in the evidence plumbing — and a speedrun origin story that undercuts the project's own packaging.

55 Minutes From Empty Repo to "Production/Stable"

The receipts, from the GitHub API and PyPI metadata:

There is no 1.0, no 1.2. The first release ever published wears 1.3.0 and "Production/Stable." An 86K-line commit is not a human timescale — it's an AI-assisted codegen burst, and the project doesn't pretend otherwise (there's no claim of human authorship anywhere). Fine. But then the version number is a costume, and the costume matters more here than usual — because this specific project's entire thesis is that unlabeled confidence is how agents get hurt. A trust-labeling system that self-labels "Production/Stable, 1.3.0" on its first release is its own first test case. It fails it.

What's Actually in the Box

The surface is enormous: 201 methods on the MathKernel facade, 168 MCP tools, nine trust levels (formal, exact, symbolic, interval_certified, numeric_high_precision, numeric, empirical, heuristic, unknown), 100+ test files, and 120+ MATHKERNEL_* environment knobs. Engines: SymPy for symbolic, Z3 for counterexamples, Lean 4 + Mathlib for formal proofs, interval arithmetic for certified enclosures.

The MCP path works end to end. I spawned mathkernel-mcp over stdio, completed the JSON-RPC handshake, listed all 168 tools, and drove math_parse → math_reason on x^2 - 2 = 0. The response carried an execution ID, a plan ID, per-obligation states with engine tags, and final_trust: symbolic. The derivation trail is real, not decorative.

graph TD
    A[Claim in] --> B[sympy: symbolic difference]
    A --> C[z3: counterexample search]
    A --> D[Lean: candidate certificate]
    B --> E[Evidence bundle]
    C --> E
    D --> E
    E --> F{conservative_trust}
    F -->|min over ALL records| G[result.trust]
    G -->|downgrade| H[status=verified / trust=unknown]

The Adversarial Suite: Every Verdict Held

I wrote a probe suite aimed at the classic failure modes of LLM math tooling:

Every verdict — refuted, verified, unknown — was correct, and every trust label on the verdict path was defensible. That's the headline most AI-generated tooling would flunk.

Two Real Cracks

1. Verified-but-unknown: the bundle eats its own verdict

Feed it sin(x)^2 + cos(x)^2 = 1. SymPy proves the difference is 0. The result arrives as status: verified — with trust: unknown and machine-readable semantic_status: candidate. I instrumented the path: the verifier returns (PROVED, SYMBOLIC), the input trust is SYMBOLIC, the derivation step records SYMBOLIC — and then MathResult's validator downgrades the whole thing (models.py, line 509):

# models.py — populate_compatible_evidence
supported_trust = TrustLevel(supported_level)
if TRUST_RANK[supported_trust.value] < TRUST_RANK[self.trust.value]:
    self.trust = supported_trust

The bundle's conservative_trust() takes the minimum over all engine records — including Z3's "unsupported fragment" attempt, which established nothing either way. An engine that declined to answer outvoted the engine that answered. "Weakest link" applied to attempts rather than established evidence. For a human reading three fields, it's confusing; for an LLM reading status: verified, it's a mixed signal the model will resolve optimistically.

2. Proof-shaped noise in refuted bundles

The refuted false identity above ships its evidence bundle with this inside:

example (x : ℚ) (y : ℚ) : ((x + y) ^ 2) = ((x ^ 2) + (y ^ 2)) := by
  ring

That's a Lean certificate claiming the ring tactic proves a false statement. It was never checked — Lean wasn't even installed — and the bundle does label the record engine: lean, trust: unknown. But the artifact sits there, proof-shaped, in the same payload as status: refuted. Any agent that scrapes lean_certificate without reading the rest ships a fabricated proof with a real-looking provenance stamp. The README warns that "a polished plot or audio artifact" doesn't create evidence — the same rule should apply to unchecked certificates: don't emit proof-shaped strings for claims you just refuted.

The Formal Engine Is a Five-Gigabyte Promise

The default prove() path auto-installs a pinned Lean 4.33.0 toolchain plus Mathlib: elan into a MathKernel-owned cache, then lake update and lake exe cache get — several gigabytes, silently, on first formal call. There's an honest opt-out (MATHKERNEL_SKIP_LEAN_INSTALL=1 reports unavailable instead of faking success), and the pins are correct. But on this box the install aborted mid-unpack twice, leaving a corrupted toolchain (a lean binary missing libInit_shared.so) behind a stale lock, and ate the disk to 100% before I wiped 3.1 GB of half-downloads. I could not complete the formal path here for resource reasons, and I'm saying so rather than rounding the gap. The design lesson stands: an MCP tool that fetches gigabytes on first invocation is a surprise an agent's operator never signed up for.

Its Own Test Suite, With Full Dependencies

On a core install ([mcp,dev]), the suite fails hard: 117–119 of 1,709 tests error across two runs — almost all ModuleNotFoundError: scipy, because test files directly import optional extras (scipy, clarabel, python-flint) without skip guards. With the full extras installed (R3_RESULT). The math that actually ran in all three runs — the symbolic, exact, interval, and Z3 paths behind my adversarial results — stayed green.

Bottom Line

MathKernel is the rare AI-speedrun artifact where the core idea survives contact: typed MathIR, nine graded trust levels, refutation-first verification, honest unknowns. If you wire it into an agent, do it in-process, set MATHKERNEL_SKIP_LEAN_INSTALL=1 until you've budgeted the formal path, and treat status, trust, and semantic_status as three separate readings — never present a lean_certificate that lacks a verified proof record behind it. The two cracks I found are both fixable in an afternoon: exclude declined engine attempts from conservative_trust, and stop emitting unchecked certificates into refuted bundles. The deeper problem is the costume. A system whose pitch is "no single trust label replaces the evidence bundle" opened its own account by labeling itself 1.3.0, Production/Stable fifty-five minutes after existing. Trust labels are cheap. Trust is the audit. Here's mine.

Related reading