GitHub - Staatsgeheim/MathKernel: Evidence-aware multi-engine mathematics runtime for LLMs: exact, symbolic, formal, certified-interval and numeric computation with typed MathIR, trust labels, and full provenance

An evidence-aware multi-engine mathematics kernel — usable both as a Python library (mathkernel) and as an MCP server (mathkernel-mcp) — so applications and LLMs can do advanced mathematics while preserving assumptions, provenance, and claim-specific evidence. The LLM interprets intent; the MathKernel establishes mathematical evidence. Mathematical results carry an explicit trust level, an engine tag, and a derivation trail. Exact computation, checked certificates, symbolic results, certified enclosures, empirical evidence, and formal proofs are distinct claims. Exact arithmetic alone is not a formal proof; approximate-input ancestry must not silently disappear. Table of contents Why Architecture Feature matrix Installation Quickstart — MCP server Quickstart — Python library Trust model Continuous symbolic mathematics Finite dynamics & PRNG analysis Engineering mathematics Geometry and topology Statistics and stochastic modeling PDEs and adaptive finite elements Relation and information-geometry inference Performance: numba · CUDA · parallelism Visualization & portable artifacts Shared multimodal projections Scientific sonification Unified multimodal artifacts MCP tool surface Configuration Repository layout Skill packages Testing Safety boundaries License Why LLMs are good at mathematical intent and bad at mathematical arithmetic. MathKernel inverts the division of labor: the model parses, plans, and interprets; the kernel computes and records claim-specific evidence. Some claims use independent certificates or cross-checks; others are exact computations in one engine. Engine agreement alone is not a proof, and a single trust label does not replace the evidence bundle. Architecture MathKernel is a typed orchestration layer rather than a single solver. The public facade owns parsing, contexts, object identity, persistence, evidence composition, resource policy and derivation tracking; domain adapters own the actual mathematics. Presentation layers sit downstream and cannot silently change the claim being made. Python / MCP | v MathKernel facade |-- parser + contexts + typed objects |-- execution/evidence contract |-- persistence + derivation graph | +--> symbolic / exact / certified / formal / numerical engines | +--> MathResult and derived mathematical objects | +--> MultimodalProjection |--> mathkernel-viz |--> mathkernel-sonify +--> unified portable artifacts This separation is deliberate: a renderer may present evidence, but it does not create stronger mathematical evidence merely by producing a polished plot or audio artifact. Feature matrix Domain Compute surface Engines Verification / evidence ceiling Symbolic algebra parse, substitute, simplify/expand/factor, solve, systems SymPy SYMBOLIC; input ancestry may lower it Calculus differentiation, integration, limits, series, sums, products SymPy SYMBOLIC + conditions Integral transforms Laplace/Fourier/Mellin/bilateral Z, inverses, ROC and property obligations typed transform adapter + SymPy SYMBOLIC; NUMERIC for approximate ancestry Complex analysis branches/domains, zeros/singularities, residues, Laurent series, contours, argument principle, continuation, conformal maps typed complex adapter + SymPy SYMBOLIC defining identities; EXACT winding certificates only for exact geometry, ancestry-capped otherwise Continuous probability typed univariate/joint/conditional distributions, transformations, marginals, Bayes, covariance, divergence, order statistics typed probability adapter + SymPy SYMBOLIC normalization/identity evidence; mathematical nonexistence retained Exact graphs typed simple/directed/weighted/multi graphs, traversal, components, shortest paths, MST, max-flow/min-cut, bipartite matching, Euler trails, coloring, topological sort, cycles, centrality, isomorphism deterministic exact graph algorithms over Fraction + njit CSR traversal kernels EXACT witness certificates; NP-hard optimality is OPTIMUM/CANDIDATE/IMPOSSIBLE/UNKNOWN, never heuristic nonexistence Exact combinatorics combinatorial classes, exact counts, lazy generation, ordinary/exponential generating functions, recurrences exact integer/Fraction enumeration + SymPy + checked njit recurrence kernels EXACT counts and recurrence/coefficient checks Finite algebra finite groups, permutation groups, abelian groups, homomorphisms, Z/nZ, GF(p^m), modules, Smith/Hermite normal forms exact algebra + SymPy combinatorics + njit Cayley/GF(p)[x] kernels EXACT axiom, homomorphism, irreducibility, and normal-form certificates Linear algebra determinant, inverse, multiply, rank, RREF, eigenvalues, exact solves SymPy EXACT for exact arithmetic; otherwise ancestry-capped Reasoning obligation-DAG planning, equivalence, counterexamples SymPy + Z3 + Lean SYMBOLIC / EXACT / FORMAL by verifier Certified numerics arbitrary-precision evaluation and interval enclosures mpmath + mpmath.iv CERTIFIED NUMERIC or NUMERIC Integers arbitrary precision, gcd/lcm, primality, factorization, CRT, modular arithmetic exact + numba batch EXACT Code generation TypeScript/Python/Rust emission, typecheck, symbolic round-trip, sandbox compilers + SymPy SYMBOLIC verification; never stronger than source Binary fields GF(2^m) arithmetic/construction and Rabin irreducibility njit n-limb kernels EXACT certificates GF(2) linear algebra rank, nullspace, powers, Berlekamp–Massey, carry-free columns bit-packed integers EXACT Discrete transforms exact FWHT with bigint fallback numba EXACT Finite dynamics Koopman/observation transfer, visibility, lagged tensors, diagnostics exact + NumPy/CuPy EXACT or NUMERIC, selected explicitly Branching Markov tensors arbitrary finite rooted Markov trees, exact leaf laws/cumulants, true-edge flattening certificates, stochastic leaf observations, channel-rank transfer, exact recovery and collective sensor fusion exact Fraction sum-product/enumeration + NumPy SVD diagnostics EXACT algebraic identities/ranks/recovery; NUMERIC singular-value and conditioning evidence kept separate Connected-relation detectability pure connected-interaction laws, stochastic mode visibility, conditional-expectation spectra, exact chi-square/Fisher retention, invisibility certificates, finite sample bounds and sensor fusion exact Fraction laws + weighted NumPy SVD + exact binomial likelihood-ratio validation EXACT transfer/information identities and lower/upper bounds; EMPIRICAL Monte Carlo checks remain separately labelled Relation-subspace visibility multi-relation Fisher Gram transfer, generalized visibility spectra, blind-combination collision certificates, cost-constrained sensor design, empirical partitions and long-run-covariance correction finite probability algebra + weighted NumPy generalized eigensystems + exact finite sensor enumeration EXACT local transfer/data-processing/collision identities; NUMERIC spectra and EMPIRICAL dependence/SkewDB checks retain explicit scope Intrinsic observation information geometry finite-simplex Fisher tangents, coordinate-invariant retained-information spectra, exact local chi-square transfer, worst-direction testing lower bounds, finite Bhattacharyya upper bounds, iid/block/cluster spectrum bootstrap, local-resolution SkewDB adapter finite probability algebra + weighted generalized eigensystems + SciPy exact-binomial validation + seeded resampling EXACT finite tangent/data-processing/divergence identities and finite simple-testing bounds; NUMERIC eigensystems and EMPIRICAL uncertainty checks remain separately labelled Composite relation inference one direction-agnostic relation-subspace test, dimension-aware finite bound, nuisance-efficient Fisher geometry, eigenspace regions, studentized/block bootstrap, HAC and misspecification diagnostics finite Fisher algebra + NumPy eigensystems + optional SciPy chi-square calibration + seeded resampling EXACT nuisance/data-processing identities and conservative bounded-score guarantee; ASYMPTOTIC composite calibration and EMPIRICAL bootstrap/dependence checks are labelled Finite Fourier cyclotomic DFT/transfer/coefficient/orbit calculations exact + NumPy FFT EXACT or NUMERIC cross-check Closure search cyclic/XOR irreducible closure relations njit meet-in-the-middle EXACT witness/exhaustive evidence Conditioned dynamics orbit access, cocycles, closures and symmetry synthesis exact enumeration + canonical rewrite EXACT witnesses Cumulants moments/cumulants and connected sample statistics exact + NumPy EXACT algebra or EMPIRICAL samples Sets & logic set algebra, membership, quantified truth and elimination SymPy sets + Z3 EXACT SMT witnesses where established Polynomial algebra Gröbner bases, division, resultants, factorization, ideal membership exact SymPy polynomial algorithms EXACT algebraic certificates Discrete probability rational RVs, Bayes, Markov quantities, seeded sampling Fraction + NumPy EXACT distributions; EMPIRICAL sampling Statistics and stochastic systems typed samples, GLMs, rank/resampling inference, survival/time-series analysis; Poisson/Wiener/GP/CTMC laws; typed Itô SDEs, Euler–Maruyama/scalar Milstein paths and coupled convergence studies typed statistical/survival/time-series/stochastic/SDE adapters + SymPy + NumPy/SciPy/mpmath EXACT identities remain separate from labelled NUMERIC fits/conditioning/exponentials and seeded EMPIRICAL resampling/simulation; no implied process/model validity, convergence theorem, population inference or causality Tensors sparse tensors, contraction and sparse solves exact + njit + CuPy EXACT or NUMERIC by arithmetic path ODEs / PDE symbolic ODE classification/dsolve; numerical IVP/named PDE solvers; typed PDE systems, weak forms, oriented simplex meshes, P1 spaces, sparse assembly, checked algebraic solves, residual–jump indicators, marking, conforming refinement, nodal transfer and observed estimator rates typed PDE/FEM/adaptivity adapters + SymPy + SciPy sparse + mpmath + njit + CUDA/CuPy estimators and empirical rates retain ancestry and never become rigorous continuum bounds or convergence