MathKernel: Een bewijsgereed multi-engine wiskunde-runtime voor LLM's

De kernfilosofie is dat het LLM de intentie interpreteert, terwijl MathKernel het wiskundige bewijs vaststelt. Wiskundige resultaten bevatten een expliciet vertrouwensniveau, een engine-tag en een afleidingsspoor. Exacte berekeningen, gecontroleerde certificaten, symbolische resultaten, gecertificeerde omsluitingen (enclosures), empirisch bewijs en formele bewijzen worden als afzonderlijke claims behandeld. Exacte rekenkunde alleen is geen formeel bewijs; de herkomst van benaderde invoer mag niet onopgemerkt verdwijnen.

Waarom MathKernel?

LLM's zijn bekwaam in wiskundige intentie, maar zwak in wiskundige rekenkunde. MathKernel draait deze arbeidsverdeling om: het model parseert, plant en interpreteert; de kernel berekent en legt claim-specifieke bewijzen vast. Sommige claims maken gebruik van onafhankelijke certificaten of kruiscontroles; andere zijn exacte berekeningen binnen één engine. Alleen overeenstemming tussen engines is geen bewijs, en een enkel vertrouwenslabel vervangt het bewijspakket niet.

Architectuur

MathKernel is een getypeerde orkestratielaag in plaats van een enkele solver. De publieke facade beheert parsing, contexten, objectidentiteit, persistentie, bewijssamenstelling, resourcebeleid en het bijhouden van afleidingen; domeinadapters beheren de eigenlijke wiskunde. Presentatielagen bevinden zich stroomafwaarts en kunnen de gemaakte claim niet stilletjes wijzigen.

Structuur: Python / MCP → MathKernel facade (parser + contexten + getypeerde objecten → executie/bewijscontract → persistentie + afleidingsgraaf) → Engines (symbolisch / exact / gecertificeerd / formeel / numeriek) → MathResult en afgeleide wiskundige objecten → MultimodalProjection (mathkernel-viz, mathkernel-sonify) → Unified portable artifacts.

Deze scheiding is bewust: een renderer kan bewijs presenteren, maar creëert geen sterker wiskundig bewijs enkel door een gepolijste plot of audio-artefact te produceren.

Feature Matrix

Domein	Compute Surface	Engines	Verificatie / Bewijsniveau
Symbolische algebra	parse, substitute, simplify/expand/factor, solve, systems	SymPy	SYMBOLIC; invoerherkomst kan dit verlagen
Calculus	differentiatie, integratie, limieten, reeksen, sommen, producten	SymPy	SYMBOLIC + condities
Integraaltransformaties	Laplace/Fourier/Mellin/bilaterale Z, inversen, ROC en eigendomsobligaties	typed transform adapter + SymPy	SYMBOLIC; NUMERIC voor benaderde herkomst
Complexe analyse	branches/domeinen, nulpunten/singulariteiten, residuen, Laurent-reeksen, contouren, argumentprincipe, continuering, conforme mappen	typed complex adapter + SymPy	SYMBOLIC voor identiteiten; EXACT winding-certificaten enkel voor exacte geometrie
Continue waarschijnlijkheid	getypeerde univ./joint/conditionele distributies, transformaties, marginalen, Bayes, covariantie, divergentie, order statistieken	typed probability adapter + SymPy	SYMBOLIC normalisatie/identiteitsbewijs
Exacte grafen	getypeerde simple/directed/weighted/multi grafen, traversal, componenten, kortste paden, MST, max-flow/min-cut, bipartite matching, Euler trails, coloring, topologische sortering, cycli, centraliteit, isomorfisme	deterministische exacte graafalgoritmen over Fraction + njit CSR traversal kernels	EXACT witness certificaten; NP-hard optimaliteit is OPTIMUM/CANDIDATE/IMPOSSIBLE/UNKNOWN
Exacte combinatoriek	combinatorische klassen, exacte tellingen, lazy generation, gewone/exponentiële genererende functies, recurrenties	exact integer/Fraction enumeration + SymPy + checked njit recurrence kernels	EXACT tellingen en recurrentie/coëfficiënt checks
Eindige algebra	eindige groepen, permutatiegroepen, abelse groepen, homomorfismen, Z/nZ, GF(p^m), modules, Smith/Hermite normal forms	exact algebra + SymPy combinatorics + njit Cayley/GF(p)[x] kernels	EXACT axioma, homomorfisme, irreducibiliteit en normal-form certificaten
Lineaire algebra	determinant, inverse, vermenigvuldigen, rank, RREF, eigenwaarden, exacte oplossingen	SymPy	EXACT voor exacte rekenkunde; anders beperkt door herkomst
Redeneren	obligation-DAG planning, equivalentie, tegenvoorbeelden	SymPy + Z3 + Lean	SYMBOLIC / EXACT / FORMAL per verifieerder
Gecertificeerde numeriek	willekeurige precisie evaluatie en interval-omsluitingen	mpmath + mpmath.iv	CERTIFIED NUMERIC of NUMERIC
Gehelen	willekeurige precisie, gcd/lcm, primality, factorisatie, CRT, modulaire rekenkunde	exact + numba batch	EXACT
Codegeneratie	TypeScript/Python/Rust emissie, typecheck, symbolische round-trip, sandbox	compilers + SymPy	SYMBOLIC verificatie
Binaire velden	GF(2^m) rekenkunde/constructie en Rabin irreducibiliteit	njit n-limb kernels	EXACT certificaten
GF(2) lineaire algebra	rank, nullspace, machten, Berlekamp–Massey, carry-free columns	bit-packed integers	EXACT
Discrete transformaties	exact FWHT met bigint fallback	numba	EXACT
Eindige dynamica	Koopman/observation transfer, visibility, lagged tensors, diagnostics	exact + NumPy/CuPy	EXACT of NUMERIC, expliciet geselecteerd
Branching Markov tensors	willekeurige eindige gewortelde Markov-bomen, exacte leaf laws/cumulants, true-edge flattening certificaten, stochastische leaf observations, channel-rank transfer, exacte recovery en collectieve sensor fusion	exact Fraction sum-product/enumeration + NumPy SVD diagnostics	EXACT algebraïsche identiteiten/ranks/recovery; NUMERIC singular-value en conditionering bewijs apart gehouden
Connected-relation detectability	pure connected-interaction laws, stochastische mode visibility, conditional-expectation spectra, exacte chi-square/Fisher retention, invisibility certificaten, finite sample bounds en sensor fusion	exact Fraction laws + weighted NumPy SVD + exact binomial likelihood-ratio validation	EXACT transfer/informatie identiteiten en lower/upper bounds; EMPIRICAL Monte Carlo checks apart gelabeld
Relation-subspace visibility	multi-relation Fisher Gram transfer, generalized visibility spectra, blind-combination collision certificaten, cost-constrained sensor design, empirische partities en long-run-covariance correctie	finite probability algebra + weighted NumPy generalized eigensystems + exact finite sensor enumeration	EXACT lokale transfer/data-processing/collision identiteiten; NUMERIC spectra en EMPIRICAL dependence/SkewDB checks behouden expliciet scope
Intrinsic observation information geometry	finite-simplex Fisher tangents, coordinate-invariant retained-information spectra, exact lokale 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 identiteiten en finite simple-testing bounds; NUMERIC eigensystems en EMPIRICAL onzekerheidschecks apart gelabeld
Composite relation inference	one direction-agnostic relation-subspace test, dimension-aware finite bound, nuisance-efficient Fisher geometry, eigenspace regions, studentized/block bootstrap, HAC en misspecification diagnostics	finite Fisher algebra + NumPy eigensystems + optional SciPy chi-square calibration + seeded resampling	EXACT nuisance/data-processing identiteiten en conservatieve bounded-score garantie; ASYMPTOTIC composite calibration en EMPIRICAL bootstrap/dependence checks gelabeld
Eindige Fourier	cyclotomische DFT/transfer/coëfficiënt/orbit berekeningen	exact + NumPy FFT	EXACT of NUMERIC cross-check
Closure search	cyclic/XOR irreducible closure relaties	njit meet-in-the-middle	EXACT witness/uitputtend bewijs
Conditioned dynamics	orbit access, cocycles, closures en symmetry synthesis	exact enumeration + canonical rewrite	EXACT witnesses
Cumulanten	momenten/cumulanten en connected sample statistieken	exact + NumPy	EXACT algebra of EMPIRICAL samples
Sets & logica	set algebra, membership, gekwantificeerde waarheid en eliminatie	SymPy sets + Z3	EXACT SMT witnesses waar vastgesteld
Polynomiale algebra	Gröbner bases, deling, resultanten, factorisatie, ideaal membership	exact SymPy polynomial algorithms	EXACT algebraïsche certificaten
Discrete waarschijnlijkheid	rationele RV's, Bayes, Markov kwantiteiten, seeded sampling	Fraction + NumPy	EXACT distributies; EMPIRICAL sampling
Statistiek en stochastische systemen	getypeerde samples, GLM's, rank/resampling inference, survival/time-series analyse; Poisson/Wiener/GP/CTMC laws; getypeerde Itô SDE's, Euler–Maruyama/scalar Milstein paths en gekoppelde convergentiestudies	typed statistical/survival/time-series/stochastic/SDE adapters + SymPy + NumPy/SciPy/mpmath	EXACT identiteiten apart van gelabelde NUMERIC fits/conditioning/exponentials en seeded EMPIRICAL resampling/simulatie
Tensors	sparse tensors, contractie en sparse solves	exact + njit + CuPy	EXACT of NUMERIC per rekenpad
ODE's / PDE	symbolische ODE classificatie/dsolve; numerieke IVP/named PDE solvers; getypeerde PDE systemen, weak forms, oriented simplex meshes, P1 spaces, sparse assembly, checked algebraic solves, residual–jump indicators, marking, conforming refinement, nodal transfer en observed estimator rates	typed PDE/FEM/adaptivity adapters + SymPy + SciPy sparse + mpmath + njit + CUDA/CuPy	estimators en empirische rates behouden herkomst en worden nooit rigoureuze continuum bounds of convergentietheorema's
Optimalisatie	kritieke punten, KKT, exact LP, numerieke nonlinear/multistart	Fraction + njit + process pool	EXACT LP certificaten of NUMERIC kandidaten
Eenheden	SI dimensies, rationele conversies en semantische-unit propagatie	exact Fraction	EXACT
Assurance	interval obligaties, Lean replay, Arb balls, persistentie en fuzzing	mpmath.iv + flint + Lean	CERTIFIED NUMERIC / FORMAL / differentieel bewijs
Theorema-bewijzen	SMT portfolio en Lean certificaten	Z3 + Lean	EXACT SMT witness of FORMAL kernel-checked bewijs
Uitputtende sweeps	Collatz en cuboid zoektochten	numba + CUDA + process pools	EXACT enkel wanneer dekking uitputtend is
Async jobs	submit/status/result/list met bewijs-behoudende retrieval	job pool	Behoudt onderliggend bewijs
Visualisatie	renderer-neutrale interactieve/statische wiskundige artefacten	Python SVG + vendored three.js	Geen nieuw bewijs; behoudt bronvertrouwen
Sonificatie	declaratieve wetenschappelijke audio mappings en deterministische WAV	Python PCM + WebAudio	Kandidaat observatie enkel
Multimodale artefacten	gesynchroniseerde visuele/audio artefact assemblage	shared artifact schema	Zwakste inbegrepen claim/bewijs
Differentiaalmeetkunde	manifolds, oriented charts, metrics, coordinate maps, tensor fields, forms, curvature, covariant/Lie/exterior derivatives, wedge/interior/pullback/Hodge operations	typed geometry adapter + SymPy	SYMBOLIC identiteiten met expliciete domeinen, Jacobians, signature en herkomst
Computationele meetkunde	concrete punten/sets, polygonen, half-space polytopes, triangulaties, hull, containment, intersection, nearest neighbor, Delaunay en Voronoi	exact SymPy determinants + adaptive float filters	EXACT topologie voor exacte coördinaten; NUMERIC enkel bij filters; anders expliciet AMBIGUOUS
Algebraïsche topologie	finite simplicial/cubical/integral chain complexes, exact triangulation conversion, oriented boundaries, Euler characteristic, homology over Z/Q/GF(p)	exact integer matrices + certified Smith normal form + rational/modular elimination	EXACT face-closure, boundary², rank-nullity, quotient, torsion en Euler–Poincaré certificaten

Getypeerde Functionaliteit

De generieke MCP-tools mathobjectcreate, mathobjectget en mathapply bieden toegang tot de volgende compositionele operaties. De mathcapability_query is de actuele bron voor parameterschema's, output-types, limieten, engines en verificatiemethoden.

Domeinen en Operaties (Selectie)

• Integraaltransformaties (TransformProblem): apply, solve, verify.
• Complexe analyse (ComplexFunction): analyticcontinuation, analyticity, argumentprinciple, classifysingularity, conformalat, conformalmap, contourintegral, derivative, laurent_series, residue, singularities, zeros.
• Continue waarschijnlijkheid (Distribution): cdf, characteristicfunction, convolve, crossentropy, entropy, expectation, kldivergence, mean, mgf, mixture, moment, orderstatistic, pdf, quantile, query, survival, truncate, variance, verify.
• Exacte grafen (Graph, MultiGraph, DirectedGraph, WeightedGraph): bfs, centrality, coloring, connectedcomponents, cycledetection, dfs, eulerpath, matching, shortestpath, verify, isomorphic_to, etc.
• Combinatoriek (CombinatorialClass, GeneratingFunction): count, generate, verify, coefficient, recurrence.
• Eindige groepen (FiniteGroup, PermutationGroup, FiniteAbelianGroup): center, centralizer, closure, commutatorsubgroup, conjugacyclasses, cosets, generated_subgroup, normality, orbits, order, quotient, stabilizers, subgroups, verify, etc.
• Eindige algebra (FiniteRing, FiniteField, Module): add, inverse, multiply, verify, hermitenormalform, smithnormalform.
• Signalen & Control (ContinuousSignal, DiscreteSignal, TransferFunction, StateSpaceSystem): bode, feedback, frequencyresponse, impulseresponse, nyquist, poles, stability, step_response, etc.
• Optimalisatie (OptimizationProblem, ConicProblem): certifymilp, solve, toconic, verify_certificate.
• Differentiaalmeetkunde (Metric, CoordinateMap, TensorField, DifferentialForm): inversemetric, christoffel, riemann, ricci, scalarcurvature, einstein, geodesicequations, jacobian, covariantderivative, liederivative, wedge, exteriorderivative, etc.
• Computationele meetkunde (Point, PointSet, Polygon, Polytope, Triangulation): distanceto, orientation, incircle, segmentintersection, convexhull, nearestneighbor, delaunay, voronoi, contains, intersection, triangulate, verify.
• Algebraïsche topologie (SimplicialComplex, CubicalComplex, ChainComplex): verify, chaincomplex, boundarymatrix, homology, euler_characteristic.
• Statistiek & Stochastiek (StatisticalSample, SurvivalDataset, TimeSeriesDataset, PoissonProcess, WienerProcess, GaussianProcess, ContinuousTimeMarkovChain): describe, covariance, empirical_distribution, fit, forecast, verify, simulate, etc.
• PDE's & FEM (PDEProblem, WeakForm, FEMMesh, FEMSolution): verify, classify, deriveweakform, solve, estimate_error, refine.

Installatie

pip install mathkernel           # Python mathematical core
pip install 'mathkernel[mcp]'    # voeg de optionele MCP transport toe

Vanaf broncode:

python -m venv .venv
source .venv/bin/activate        # Windows: .venv\Scripts\activate
pip install -e .                # Python mathematical core
pip install -e '.[mcp]'         # voeg de optionele MCP transport toe

Optionele extra's:

• pip install -e '.[perf]': Numba JIT kernels.
• pip install -e '.[cuda]': CuPy + NVIDIA runtime libraries (voor RTX GPU's).
• pip install -e '.[latex]': ANTLR4 runtime voor mathparselatex.
• pip install -e '.[dev]': Pytest.

Opmerking over Lean 4: Lean 4 + Mathlib wordt standaard geïnstalleerd bij de eerste start van mathkernel-mcp. Sla dit over met MATHKERNELSKIPLEAN_INSTALL=1.

Snelstart

MCP-server

De server communiceert via MCP over stdio (FastMCP 3). Er zijn 162 tools beschikbaar, allemaal beginnend met math_.

Voorbeeld sessie:

1. math_capabilities → Ontdek surface, limieten en engines.
2. mathparse("x^2 - 3*x + 2 = 0") → Geeft exprid.
3. mathcontextcreate(domains={"x": "real"}) → Geeft context_id.
4. mathreason(exprid, context_id, formal=true) → Lost op en verifieert onafhankelijk.
5. mathderivationtrace(step_id) → Volledige provenance op aanvraag.

Lange sweeps zijn asynchroon: mathjobsubmit → mathjobstatus → mathjobresult.

Python-bibliotheek

De MCP-server is een dunne transportlaag; alle functies zijn direct in-process beschikbaar:

from mathkernel import MathKernel
kernel = MathKernel()

# Symbolisch
r = kernel.parse("x^2 - 2 = 0")
sol = kernel.solve(r.data["expr_id"], "x")
assert sol.ok and sol.trust.value == "symbolic"

# Exacte GF(2^m) veldrekenkunde
f = kernel.gf2m_create(8, "1b")  # AES polynoom
kernel.gf2m_compute(f.data["field_id"], "mul", ["53", "ca"])

Vertrouwensmodel

Het vertrouwensniveau wordt bepaald door het zwakste bewijs dat nodig is om het resultaat vast te stellen:

• formal: Lean-certificaat geaccepteerd door de Lean-kernel.
• exact: Exacte berekening / gecontroleerd claim-specifiek certificaat.
• symbolic: Overeenstemming tussen symbolische engines (bijv. SymPy residu-checks).
• interval_certified: Rigoureuze omsluiting (mpmath interval).
• numerichighprecision: Numeriek met willekeurige precisie.
• numeric: Float-bewijs (inclusief GPU fast paths).
• empirical / heuristic / unknown: Empirisch, heuristisch of onbekend.

Belangrijke regels:

• Onafhankelijke onenigheid tussen backends wordt bewaard als een expliciet conflict.
• Decimale literalen worden behandeld als benaderde observaties en beperken het vertrouwen vanaf de parsing-fase tot numeric.
• Formele certificaten en exacte SMT-tegenvoorbeelden worden geweigerd voor benaderde invoer.

Domeinspecificaties

Continue symbolische wiskunde

Gebruikt getypeerde objecten en een object_create → apply model. Elke operatie registreert een DAG met vier obligaties: getypeerde-invoervalidatie, kandidaatberekening, domein-invariant verificatie en conservatieve bewijsreconciliatie.

• Integraaltransformaties: Laplace, Fourier, Mellin en bilaterale Z-transformaties met expliciete conventies en convergentiegebieden (ROC).
• Complexe analyse: Afgeleiden, analyticity, nulpunten, singulariteiten, Laurent-reeksen, residuen en conforme mappen.
• Continue waarschijnlijkheid: Getypeerde univariate, joint en conditionele distributies; PDF/CDF, momenten, entropie en Bayes-conditionering.

Eindige dynamica & PRNG-analyse

Biedt exacte spectrale analyse van eindige dynamische systemen, specifiek voor PRNG-structuuranalyse.

• Koopman suite: Transportmatrix $Q$, observatie-transfer $C$, mode visibility $\rho_O$ en lagged state tensors.
• Stochastische observatie-transfer: Exacte FiniteJointLaw contracties en Markov-pad momenten.
• Branching General Markov tensors: Sum-product wetten op heterogene gewortelde bomen.
• Statistische fylogenetische inferentie: Projectie op de waarschijnlijkheids-simplex en multinomiale covariantie.

Technische wiskunde

Biedt getypeerde instrumenten voor signalen, controlesystemen en geconstreineerde optimalisatie.

• Signalen: FIR/IIR filters met behoud van coëfficiënten en conventies.
• Control Systems: SISO/MIMO modellen, LQR, Kalman-filtering en MPC (Model Predictive Control).
• Optimalisatie: Exacte optimality witnesses voor LP/QP; Farkas-certificaten voor onhaalbare LP's.

Meetkunde en topologie

• Differentiaalmeetkunde: Manifolds, metrics en tensorcalculus. Berekeningen van Christoffel-symbolen, Riemann/Ricci-curvatuur en geodetische vergelijkingen.
• Computationele meetkunde: Exacte oriëntatie, convex hulls, Delaunay-triangulatie en Voronoi-diagrammen.
• Algebraïsche topologie: Simplicial/Cubical complexes, boundary matrices en homologe berekeningen over $\mathbb{Z}, \mathbb{Q}$ of $GF(p)$.

Statistiek en stochastische modellering

• Samples: StatisticalSample bewaart concrete observaties en metadata.
• GLM's: Ondersteuning voor Gaussian/identity, binomial/logit en Poisson/log.
• Non-parametrische tests: Mann-Whitney, Wilcoxon, Kruskal-Wallis, etc.
• Survival analyse: Kaplan-Meier schattingen en Cox Proportional Hazards modellen.
• Tijdreeksen: ACF/PACF, stationariteitstests en ARIMA/GARCH modellen.
• Stochastische processen: Poisson, Wiener, Gaussian processen en CTMC's.
• SDE's: Itô systemen met Euler-Maruyama en Milstein simulaties.

PDE's en adaptieve eindige elementen (FEM)

• PDE Representatie: Classificatie van systemen en compatibiliteitschecks voor randvoorwaarden.
• Weak Forms: Expliciete representatie van zwakke formuleringen en integratie-per-delen.
• FEM: Ondersteuning voor simplex meshes (driehoeken/tetraëders), P1 Lagrange functies en sparse assembly.
• Adaptiviteit: Residual-jump indicatoren en Dörfler-marking voor mesh-verfijning.

Performance: Numba, CUDA en Parallelisme

Workload	CPU Fast Path	GPU Path	Parallel
Collatz sieve	njit ($n \le 31$)	CUDA RawKernel	process pool
Cuboid sweep	njit scan + QR filter	CUDA RawKernel	process pool
GF($2^m$) $\le 1024$	njit n-limb kernels	—	—
Integer batch	njit array kernels	—	process pool
Koopman / dynamics	numpy complex128	CuPy matmul	—
Obligation DAG	—	—	thread waves

Visualisatie en Artefacten

Visualisatie (mathkernel_viz)

Zet MathKernel-objecten om in interactieve artefacten. Visualisatie is stroomafwaarts: het consumeert data maar verhoogt nooit het vertrouwensniveau van de bron.

• Portable HTML: Zelfstandige bestanden met embedded datasets en provenance; geen server of CDN nodig.
• Interactief 3D: Orbit/pan/zoom en inspectie van identiteit en vertrouwen.

Sonificatie (mathkernel-sonify)

De auditieve tegenhanger van visualisatie. Het zet wiskundige resultaten om in audio via declaratieve mappings (bijv. spectrum → geluid). Een hoorbaar patroon is een "perceptuele kandidaat" en geen wiskundig bewijs.

Multimodale Artefacten (mathkernel-multimodal)

Combineert visuele en auditieve representaties in één MathKernelArtifact. Dit maakt gesynchroniseerde analyse mogelijk waarbij visuele blokken oplichten tijdens audio-afspeelbaarheid.

Configuratie

Instellingen worden aangestuurd via omgevingsvariabelen met het prefix MATHKERNEL_.

Belangrijke variabelen (selectie):

• MATHKERNELMAXINPUT_LENGTH: Limiet voor parser input (default: 100.000).
• MATHKERNELSOLVERTIMEOUT_SECONDS: Budget voor symbolische operaties (default: 30).
• MATHKERNELENABLEEXECUTION: Activeert sandboxed codegen executie (default: false).
• MATHKERNELZ3TIMEOUT_MS: Budget voor SMT-solver (default: 10.000).
• MATHKERNELSTOREPATH: Pad voor SQLite persistentie.

Veiligheidsgrenzen

• Parsing: Geen ruwe gebruikersuitdrukkingen in sympify(); gebruik van een beperkte grammatica.
• Executie: Sandboxed code-executie is opt-in en draait in een geïsoleerd subprocess met timeout.
• Integriteit: SQLite-persistentie controleert elk JSON-payload met SHA-256 vóór decodering.
• Isolatie: Externe solvers (LP/QP/MILP) draaien in verse interpreters die bij timeout worden beëindigd.

Licentie

Copyright © 2026 Maarten Boone. Uitgegeven onder de MIT-licentie.