MathKernel: 証拠認識型マルチエンジン数学カーネルおよびMCPサーバー

MathKernel 証拠認識型マルチエンジン数学カーネル — Pythonライブラリ（mathkernel）およびMCPサーバー（mathkernel-mcp）として使用可能 — アプリケーションやLLMが、仮定、来歴、および主張固有の証拠を維持しながら高度な数学を実行できるようにします。LLMは意図を解釈し、MathKernelは数学的証拠を確立します。数学的な結果には、明示的な信頼レベル、エンジンタグ、および導出パスが付与されます。正確な計算、検証済み証明書、記号結果、証明付き区間、経験的証拠、および形式証明は、区別される主張です。正確な算術演算だけでは形式証明ではなく、近似入力の祖先が静かに消えてはなりません。 目次 なぜ アーキテクチャ 機能マトリックス インストール クイックスタート — MCPサーバー クイックスタート — Pythonライブラリ 信頼モデル 連続シンボリック数学 有限ダイナミクスとPRNG分析 エンジニアリング数学 幾何学とトポロジー 統計と確率モデリング PDEと適応有限要素 関係と情報幾何学的推論 パフォーマンス: numba · CUDA · 並列処理 可視化とポータブルアーティファクト 共有マルチモーダル投影 科学的ソニフィケーション 統一マルチモーダルアーティファクト MCPツールサーフェス 設定 リポジトリレイアウト スキルパッケージ テスト 安全境界 ライセンス なぜLLMは数学的意図には優れているが、数学的算術には劣るのか。 MathKernelは労働の分担を逆転させます。モデルが解析、計画、解釈を行い、カーネルが計算して主張固有の証拠を記録します。一部の主張は独立した証明書またはクロスチェックを使用し、その他は単一エンジンでの正確な計算です。単なるエンジンの合意は証明ではなく、単一の信頼ラベルは証拠バンドルに取って代わるものではありません。 アーキテクチャ MathKernelは、単一のソルバーではなく、型付けされたオーケストレーションレイヤーです。パブリックファサードは、解析、コンテキスト、オブジェクトID、永続化、証拠構成、リソースポリシー、および導出追跡を所有し、ドメインアダプターは実際の数学を所有します。プレゼンテーションレイヤーは下流に位置し、主張されている内容を静かに変更することはできません。 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 この分離は意図的です。レンダラーは証拠を提示できますが、洗練されたプロットやオーディオアーティファクトを生成するだけで、より強力な数学的証拠を作成するわけではありません。 機能マトリックス ドメイン | 計算サーフェス | エンジン | 検証 / 証拠の天井 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 | 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 | 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 F