MathKernel-MCP

MathKernel

Um kernel matemático multi-motor com consciência de evidências — utilizável tanto como biblioteca Python (mathkernel) quanto como servidor MCP (mathkernel-mcp) — para que aplicações e LLMs possam fazer matemática avançada preservando suposições, proveniência e evidências específicas de cada afirmação.

O LLM interpreta a intenção; o MathKernel estabelece a evidência matemática.

Resultados matemáticos carregam um nível de confiança explícito, uma etiqueta de motor e um rastro de derivação. Cálculo exato, certificados verificados, resultados simbólicos, enclausuramentos certificados, evidência empírica e provas formais são afirmações distintas. Aritmética exata por si só não é uma prova formal; a ancestralidade de entradas aproximadas não deve desaparecer silenciosamente.

---

Sumário

• Por quê
• Arquitetura
• Matriz de recursos
• Instalação
• Início rápido — servidor MCP
• Início rápido — biblioteca Python
• Modelo de confiança
• Matemática simbólica contínua
• Dinâmica finita e análise de PRNG
• Matemática para engenharia
• Geometria e topologia
• Estatística e modelagem estocástica
• EDPs e elementos finitos adaptativos
• Inferência de relações e geometria da informação
• Desempenho: numba · CUDA · paralelismo
• Visualização e artefatos portáteis
• Projeções multimodais compartilhadas
• Sonificação científica
• Artefatos multimodais unificados
• MathKernel Studio
• Superfície de ferramentas MCP
• Configuração
• Estrutura do repositório
• Pacotes de habilidades
• Testes
• Limites de segurança
• Licença

Por quê

LLMs são bons em intenção matemática e ruins em aritmética matemática. O MathKernel inverte a divisão de trabalho: o modelo analisa, planeja e interpreta; o kernel calcula e registra evidências específicas de cada afirmação. Algumas afirmações usam certificados independentes ou verificações cruzadas; outras são cálculos exatos em um único motor. A concordância entre motores por si só não é uma prova, e um único rótulo de confiança não substitui o pacote de evidências.

Arquitetura

O MathKernel é uma camada de orquestração tipada, e não um único solucionador. A fachada pública é responsável por análise sintática, contextos, identidade de objetos, persistência, composição de evidências, política de recursos e rastreamento de derivação; os adaptadores de domínio são responsáveis pela matemática em si. As camadas de apresentação ficam a jusante e não podem alterar silenciosamente a afirmação que está sendo feita.

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

Essa separação é deliberada: um renderizador pode apresentar evidências, mas não cria evidências matemáticas mais fortes apenas por produzir um gráfico polido ou um artefato de áudio.

Matriz de recursos

Domínio	Superfície de computação	Motores	Teto de verificação / evidência
Álgebra simbólica	parse, substituir, simplificar/expandir/fatorar, resolver, sistemas	SymPy	SYMBOLIC; ancestralidade da entrada pode reduzi-lo
Cálculo	diferenciação, integração, limites, séries, somas, produtos	SymPy	SYMBOLIC + condições
Transformadas integrais	Laplace/Fourier/Mellin/Z bilateral, inversas, ROC e obrigações de propriedade	adaptador de transformada tipada + SymPy	SYMBOLIC; NUMERIC para ancestralidade aproximada
Análise complexa	ramos/domínios, zeros/singularidades, resíduos, séries de Laurent, contornos, princípio do argumento, continuação, mapas conformes	adaptador complexo tipado + SymPy	identidades definidoras SYMBOLIC; certificados EXACT de winding apenas para geometria exata, limitados pela ancestralidade caso contrário
Probabilidade contínua	distribuições univariadas/conjuntas/condicionais tipadas, transformações, marginais, Bayes, covariância, divergência, estatísticas de ordem	adaptador de probabilidade tipado + SymPy	evidência de normalização/identidade SYMBOLIC; inexistência matemática preservada
Grafos exatos	grafos simples/dirigidos/ponderados/multigrafos tipados, travessia, componentes, caminhos mais curtos, MST, fluxo máximo/corte mínimo, emparelhamento bipartido, trilhas de Euler, coloração, ordenação topológica, ciclos, centralidade, isomorfismo	algoritmos determinísticos exatos de grafos sobre Fraction + kernels de travessia CSR njit	certificados de testemunha EXACT; otimalidade NP-difícil é OPTIMUM/CANDIDATE/IMPOSSIBLE/UNKNOWN, nunca inexistência heurística
Combinatória exata	classes combinatórias, contagens exatas, geração preguiçosa, funções geradoras ordinárias/exponenciais, recorrências	enumeração exata de inteiros/Fraction + SymPy + kernels de recorrência njit verificados	contagens EXACT e verificações de recorrência/coeficiente
Álgebra finita	grupos finitos, grupos de permutação, grupos abelianos, homomorfismos, Z/nZ, GF(p^m), módulos, formas normais de Smith/Hermite	álgebra exata + combinatória SymPy + kernels njit de Cayley/GF(p)[x]	certificados EXACT de axioma, homomorfismo, irredutibilidade e forma normal
Álgebra linear	determinante, inversa, multiplicar, posto, RREF, autovalores, soluções exatas	SymPy	EXACT para aritmética exata; caso contrário, limitado pela ancestralidade
Raciocínio	planejamento de DAG de obrigações, equivalência, contraexemplos	SymPy + Z3 + Lean	SYMBOLIC / EXACT / FORMAL por verificador
Numérica certificada	avaliação de precisão arbitrária e envoltórios intervalares	mpmath + mpmath.iv	CERTIFIED NUMERIC ou NUMERIC
Inteiros	precisão arbitrária, gcd/lcm, primalidade, fatoração, CRT, aritmética modular	exato + numba em lote	EXACT
Geração de código	emissão TypeScript/Python/Rust, verificação de tipos, round-trip simbólico, sandbox	compiladores + SymPy	verificação SYMBOLIC; nunca mais forte que a fonte
Campos binários	aritmética/construção GF(2^m) e irredutibilidade de Rabin	kernels njit de n-limbos	certificados EXACT
Álgebra linear GF(2)	posto, espaço nulo, potências, Berlekamp–Massey, colunas sem transporte	inteiros empacotados em bits	EXACT
Transformadas discretas	FWHT exato com fallback bigint	numba	EXACT
Dinâmica finita	transferência Koopman/observação, visibilidade, tensores defasados, diagnósticos	exato + NumPy/CuPy	EXACT ou NUMERIC, selecionado explicitamente
Tensores de Markov ramificados	árvores de Markov finitas enraizadas arbitrárias, leis exatas de folhas/cumulantes, certificados de achatamento de arestas verdadeiras, observações estocásticas de folhas, transferência de posto de canal, recuperação exata e fusão coletiva de sensores	soma-produto/enumeração exata Fraction + diagnósticos SVD NumPy	identidades algébricas/postos/recuperação EXACT; evidência NUMERIC de valores singulares e condicionamento mantida separada
Detectabilidade de relação conectada	leis puras de interação conectada, visibilidade estocástica de modos, espectros de expectativa condicional, retenção exata qui-quadrado/Fisher, certificados de invisibilidade, limites finitos de amostra e fusão de sensores	leis exatas Fraction + SVD NumPy ponderado + validação exata de razão de verossimilhança binomial	identidades de transferência/informação EXACT e limites inferior/superior; verificações EMPIRICAL de Monte Carlo permanecem rotuladas separadamente
Visibilidade de subespaço de relação	transferência de Gram Fisher multi-relação, espectros de visibilidade generalizados, certificados de colisão de combinação cega, projeto de sensores com restrição de custo, partições empíricas e correção de covariância de longo prazo	álgebra de probabilidade finita + sistemas de autovalores generalizados NumPy ponderados + enumeração exata finita de sensores	identidades EXACT de transferência local/processamento de dados/colisão; espectros NUMERIC e verificações EMPIRICAL de dependência/SkewDB retêm escopo explícito
Geometria de informação de observação intrínseca	tangentes Fisher de simplex finito, espectros de informação retida invariantes a coordenadas, transferência exata local qui-quadrado, limites inferiores de teste na pior direção, limites superiores finitos de Bhattacharyya, bootstrap de espectro iid/bloco/cluster, adaptador SkewDB de resolução local	álgebra de probabilidade finita + sistemas de autovalores generalizados ponderados + validação exata binomial SciPy + reamostragem com semente	identidades EXACT de tangente finita/processamento de dados/divergência e limites finitos de teste simples; sistemas de autovalores NUMERIC e verificações de incerteza EMPIRICAL permanecem rotulados separadamente
Inferência de relação composta	um teste de subespaço de relação agnóstico a direção, limite finito ciente de dimensão, geometria Fisher eficiente a incômodos, regiões de autoespaço, bootstrap studentizado/bloco, diagnósticos HAC e de especificação incorreta	álgebra Fisher finita + sistemas de autovalores NumPy + calibração qui-quadrado opcional SciPy + reamostragem com semente	identidades EXACT de incômodo/processamento de dados e garantia conservadora de pontuação limitada; calibração composta ASYMPTOTIC e verificações EMPIRICAL de bootstrap/dependência são rotuladas
Fourier finito	cálculos ciclotômicos de DFT/transferência/coeficiente/órbita	exato + FFT NumPy	EXACT ou verificação cruzada NUMERIC
Busca de fechamento	relações de fechamento irredutíveis cíclicas/XOR	njit meet-in-the-middle	evidência EXACT de testemunha/exaustiva
Dinâmica condicionada	acesso a órbitas, cociclos, fechamentos e síntese de simetria	enumeração exata + reescrita canônica	testemunhas EXACT
Cumulantes	momentos/cumulantes e estatísticas de amostra conectadas	exato + NumPy	álgebra EXACT ou amostras EMPIRICAL
Conjuntos e lógica	álgebra de conjuntos, pertinência, verdade quantificada e eliminação	conjuntos SymPy + Z3	testemunhas EXACT SMT onde estabelecidas
Álgebra polinomial	bases de Gröbner, divisão, resultantes, fatoração, pertinência a ideais	algoritmos polinomiais exatos SymPy	certificados algébricos EXACT
Probabilidade discreta	VAs racionais, Bayes, quantidades de Markov, amostragem com semente	Fraction + NumPy	distribuições EXACT; amostragem EMPIRICAL
Estatística e sistemas estocásticos	amostras tipadas, GLMs, inferência por posto/reamostragem, análise de sobrevivência/séries temporais; leis de Poisson/Wiener/GP/CTMC; SDEs de Itô tipadas, caminhos Euler–Maruyama/Milstein escalar e estudos de convergência acoplados	adaptadores tipados estatísticos/sobrevivência/séries temporais/estocásticos/SDE + SymPy + NumPy/SciPy/mpmath	identidades EXACT permanecem separadas de ajustes/condicionamento/exponenciais NUMERIC rotulados e reamostragem/simulação EMPIRICAL com semente; sem validade implícita de processo/modelo, teorema de convergência, inferência populacional ou causalidade
Tensores	tensores esparsos, contração e soluções esparsas	exato + njit + CuPy	EXACT ou NUMERIC por caminho aritmético
EDOs / EDPs	classificação simbólica de EDOs/dsolve; solvers numéricos de PVI/EDPs nomeadas; sistemas de EDP tipados, formas fracas, malhas de simplex orientadas, espaços P1, montagem esparsa, soluções algébricas verificadas, indicadores residual-salto, marcação, refinamento conforme, transferência nodal e taxas de estimador observadas	adaptadores tipados de EDP/FEM/adaptatividade + SymPy + SciPy esparso + mpmath + njit + CUDA/CuPy	estimadores e taxas empíricas retêm ancestralidade e nunca se tornam limites contínuos rigorosos ou teoremas de convergência
Otimização	pontos críticos, KKT, LP exato, não linear numérico/multistart	Fraction + njit + pool de processos	certificados EXACT de LP ou candidatos NUMERIC
Unidades	dimensões SI, conversões racionais e propagação de unidades semânticas	Fraction exato	EXACT
Garantia	obrigações intervalares, replay Lean, bolas Arb, persistência e fuzzing	mpmath.iv + flint + Lean	CERTIFIED NUMERIC / FORMAL / evidência diferencial
Prova de teoremas	portfólio SMT e certificados Lean	Z3 + Lean	testemunha EXACT SMT ou prova FORMAL verificada por kernel
Varreduras exaustivas	buscas de Collatz e cuboides	numba + CUDA + pools de processos	EXACT apenas quando a cobertura é exaustiva
Tarefas assíncronas	enviar/status/resultado/listar com recuperação que preserva evidência	pool de tarefas	Preserva a evidência subjacente
Visualização	artefatos matemáticos interativos/estáticos neutros a renderizador	Python SVG + three.js embutido	Sem nova evidência; preserva a confiança da fonte
Sonificação	mapeamentos declarativos de áudio científico e WAV determinístico	Python PCM + WebAudio	Apenas observação candidata
Artefatos multimodais	montagem sincronizada de artefatos visuais/áudio	esquema compartilhado de artefatos	Reivindicação/evidência incluída mais fraca
Geometria diferencial	variedades, cartas orientadas, métricas, mapas de coordenadas, campos tensoriais, formas, curvatura, derivadas covariante/Lie/exterior, operações de cunha/interior/pullback/Hodge	adaptador de geometria tipado + SymPy	identidades SYMBOLIC com domínios explícitos, Jacobianos, assinatura e ancestralidade; entrada numérica permanece NUMERIC
Geometria computacional	pontos/conjuntos concretos, polígonos, politopos de semiespaço, triangulações, envoltória, contenção, interseção, vizinho mais próximo, Delaunay e Voronoi	determinantes exatos SymPy + filtros de ponto flutuante adaptativos	topologia EXACT para coordenadas exatas; NUMERIC apenas quando filtros decidem; caso contrário, resultado AMBIGUOUS explícito
Topologia algébrica	complexos de cadeia simpliciais/cúbicos/integrais finitos, conversão exata de triangulação, fronteiras orientadas, característica de Euler, homologia sobre Z/Q/GF(p)	matrizes inteiras exatas + forma normal de Smith certificada + eliminação racional/modular	certificados EXACT de fechamento de face, fronteira², posto-nulidade, quociente, torção e Euler–Poincaré

Superfície de funcionalidade tipada

As ferramentas MCP genéricas math_object_create, math_object_get e math_apply expõem as seguintes operações composicionais. Este é o inventário completo de operações tipadas; math_capability_query é a fonte viva dos esquemas de parâmetros, tipos de saída, limites, motores e métodos de verificação.

Domínio	Objeto	Operações
Transformadas integrais	TransformProblem	apply, solve, verify
Análise complexa	ComplexFunction	analytic_continuation, analyticity, argument_principle, classify_singularity, conformal_at, conformal_map, contour_integral, derivative, laurent_series, residue, singularities, zeros
Análise complexa	Contour	winding_number
Probabilidade contínua	Distribution	cdf, characteristic_function, convolve, cross_entropy, entropy, expectation, kl_divergence, mean, mgf, mixture, moment, order_statistic, pdf, quantile, query, survival, truncate, variance, verify
Probabilidade contínua	JointDistribution	bayes, condition, correlation, covariance, marginal, order_statistic, verify
Probabilidade contínua	ConditionalDistribution, RandomVariable	condicional cdf/mean/pdf/variance/verify; variável aleatória transform
Grafos exatos	Graph, MultiGraph	bfs, centrality, coloring, connected_components, cycle_detection, dfs, euler_path, matching, shortest_path, verify; Graph também possui isomorphic_to
Grafos exatos	DirectedGraph	bfs, centrality, cycle_detection, dfs, shortest_path, strongly_connected_components, topological_sort, verify
Grafos exatos	WeightedGraph	bfs, centrality, coloring, connected_components, cycle_detection, dfs, euler_path, matching, maximum_flow, minimum_cut, minimum_spanning_tree, shortest_path, strongly_connected_components, topological_sort, verify
Combinatória	CombinatorialClass, GeneratingFunction	classe count/generate/verify; função geradora coefficient/recurrence/verify
Grupos finitos	FiniteGroup	center, centralizer, closure, commutator_subgroup, conjugacy_classes, cosets, generated_subgroup, normality, orbits, order, quotient, stabilizers, subgroups, verify
Grupos finitos	PermutationGroup	contains, orbits, order, stabilizer_chain, stabilizers, verify
Grupos finitos	FiniteAbelianGroup, GroupHomomorphism	abeliano order/verify; homomorfismo image/kernel/verify
Álgebra finita	FiniteRing, FiniteField	add, inverse, multiply, verify
Álgebra finita	Module	abelian_group, hermite_normal_form, smith_normal_form, verify
Sinais	ContinuousSignal, DiscreteSignal	contínuo sample; discreto autocorrelation, convolution, correlation, cross_spectrum, dft, resample, stft, window
Sinais	Spectrum, Filter, FilterDesign, FilterState	espectro idft; filtro apply_signal/initial_state/to_transfer_function; projeto design; estado process
Controle	TransferFunction	bode, feedback, frequency_response, impulse_response, nyquist, poles, root_locus, series, stability, step_response, to_filter, to_state_space, to_zero_pole_gain, zeros
Controle	StateSpaceSystem	bode, coefficient_units, controllability, discretize, finite_lqr, frequency_response, kalman, kalman_state, lqg, lqr, mpc, nyquist, observability, observer, place_poles, poles, stability, state_feedback, to_discrete_control, to_transfer_function, zeros
Controle	DiscreteControlSystem	bode, controllability, frequency_response, nyquist, observability, poles, stability, to_state_space, to_transfer_function, zeros
Controle	ZeroPoleGain, TransferMatrix	ZPK bode/nyquist/poles/to_transfer_function/zeros; matriz entry
Controle sequencial	FiniteHorizonLQR, KalmanState, MPCPlan	LQR control/rollout/verify; Kalman predict/update; MPC first_control/verify
Otimização	OptimizationProblem	certify_milp, solve, to_conic, verify_certificate, verify_milp_certificate
Otimização	ConicProblem, QuadraticallyConstrainedProblem	solve, verify_certificate
Geometria diferencial	Metric	inverse_metric, christoffel, riemann, ricci, scalar_curvature, einstein, geodesic_equations
Geometria diferencial	CoordinateMap	jacobian, verify
Geometria diferencial	TensorField	covariant_derivative, lie_derivative
Geometria diferencial	DifferentialForm	wedge, exterior_derivative, interior_product, pullback, hodge_star
Geometria computacional	Point	distance_to
Geometria computacional	PointSet	orientation, incircle, segment_intersection, convex_hull, nearest_neighbor, delaunay, voronoi
Geometria computacional	Polygon	verify, contains, intersection, triangulate
Geometria computacional	Polytope	verify, contains
Geometria computacional	Triangulation	verify, to_simplicial_complex
Topologia algébrica	SimplicialComplex, CubicalComplex	verify, chain_complex, boundary_matrix, homology
Topologia algébrica	ChainComplex	verify, boundary_matrix, homology, euler_characteristic
Evidência estatística e inferência	StatisticalSample	describe, covariance, empirical_distribution, evidence_profile, mann_whitney, wilcoxon, kruskal_wallis, ks_2samp, spearman, kendall, permutation_test, bootstrap
Análise de sobrevivência	SurvivalDataset	verify, kaplan_meier
Análise de sobrevivência	KaplanMeierEstimate	verify, survival_at
Análise de sobrevivência	CoxProportionalHazardsModel	verify, fit
Análise de sobrevivência	CoxPHFit	verify, diagnostics, predict_partial_hazard
Séries temporais	TimeSeriesDataset	verify, acf, pacf, stationarity_test
Séries temporais	TimeSeriesAnalysis	verify
Séries temporais	TimeSeriesModel	verify, fit
Séries temporais	TimeSeriesFit	verify, diagnostics, forecast
Séries temporais	TimeSeriesForecast	verify
Processos estocásticos	PoissonProcess	verify, pmf, moments, increment_distribution
Processos estocásticos	WienerProcess	verify, finite_dimensional, increment_distribution
Processos estocásticos	GaussianProcess	verify, finite_dimensional, condition
Processos estocásticos	ContinuousTimeMarkovChain	verify, transition_matrix, distribution, stationary_distribution
Resultados de processos estocásticos	FiniteDimensionalDistribution, GaussianProcessPosterior, CTMCTransition	verify
Equações diferenciais estocásticas	StochasticDifferentialEquation	verify, simulate, convergence_study
Simulações de EDE	SDESimulation	verify, path, terminal_values
Convergência de EDE	SDEConvergenceStudy	verify
Modelos lineares generalizados	GeneralizedLinearModel	verify, fit
Modelos lineares generalizados	GLMFit	verify, diagnostics, predict
Resultados não paramétricos	NonparametricTestResult, ResamplingResult	verify
Equações diferenciais parciais	PDEProblem	verify, classify, boundary_compatibility, derive_weak_form
Resultados de EDP	PDEClassification, PDECompatibilityReport	verify
Formulações fracas	WeakForm	verify
Malha de elementos finitos	FEMMesh	verify, reference_element, finite_element_space
Elemento de referência	ReferenceElement	verify, basis, quadrature
Resultados de elementos finitos	BasisFunctionSet, QuadratureRule, FiniteElementSpace	verify
Álgebra de MEF	AssembledSystem	verify, solve
Solução de MEF	FEMSolution	verify, estimate_error
Estimativa de erro de MEF	FEMErrorEstimate	verify, mark, compare
Refinamento	RefinementMarking	verify, refine
Malha refinada	RefinedMesh	verify, reference_element, finite_element_space
Transferência de malha / convergência	MeshTransfer, FEMConvergenceObservation	verify

Os objetos de origem usam o mesmo limite: objetos de transformada/complexo/probabilidade, grafos e estruturas combinatórias, grupos/aneis/corpos/modulos finitos, sinais/filtros/sistemas de controle, problemas de otimização e Manifold → Chart → Metric/CoordinateMap/TensorField/DifferentialForm, além de Point/PointSet/Polygon/Polytope/Triangulation, e finitos SimplicialComplex/CubicalComplex/integral ChainComplex, e observações StatisticalSample tipadas, especificações GeneralizedLinearModel, e fontes de sobrevivência SurvivalDataset/CoxProportionalHazardsModel, além de fontes de tempo ordenado TimeSeriesDataset/TimeSeriesModel, e fontes de lei de processo PoissonProcess/WienerProcess/GaussianProcess/ContinuousTimeMarkovChain, modelos Itô StochasticDifferentialEquation, e equações/domínios/condições PDEProblem estruturados. NonparametricTestResult, ResamplingResult, KaplanMeierEstimate, GLMFit, e CoxPHFit são registros somente derivados, vinculados à origem, com reprodução determinística exata, numérica ou de fluxo com semente. TimeSeriesAnalysis, TimeSeriesFit, e TimeSeriesForecast, FiniteDimensionalDistribution, GaussianProcessPosterior, e CTMCTransition seguem o mesmo limite de reprodução somente de saída. PDEClassification, PDECompatibilityReport, e WeakForm reproduzem seu resultado de parte principal, traço representado ou identidade fraca completa a partir do problema de origem. FEMMesh vincula essa forma fraca e uma triangulação verificada opcional. ReferenceElement, BasisFunctionSet, QuadratureRule, e FiniteElementSpace são somente de saída com ancestralidade reproduzível de origem única ou múltipla. AssembledSystem retém contribuições globais locais e esparsas, além de suas fontes de espaço/quadratura; FEMSolution somente de saída retém a fonte exata do sistema montado e diagnósticos de solucionador reproduzíveis. Registros somente de saída G.5 FEMErrorEstimate, RefinementMarking, RefinedMesh, MeshTransfer, e FEMConvergenceObservation retêm a cadeia completa de solução para malha filha, política de marcação, células pai/filho, pesos de interpolação e entradas de taxa empírica. SDESimulation e SDEConvergenceStudy adicionalmente reproduzem seus fluxos PCG64 e discretizações. Tipos somente derivados não podem ser forjados por meio de entrada pública.

Instalação

pip install mathkernel           # Python mathematical core
pip install 'mathkernel[mcp]'    # add the optional MCP transport

A partir de um checkout do código-fonte:

python -m venv .venv
source .venv/bin/activate        # Windows: .venv\Scripts\activate
pip install -e .           # Python mathematical core
pip install -e '.[mcp]'  # add the optional MCP transport

Extras opcionais:

pip install -e '.[perf]'    # numba — JIT kernels (sieves, GF(2^m), FWHT, closure search)
pip install -e '.[cuda]'    # CuPy + all nvidia-*-cu12 runtime libraries (RTX-class GPU)
pip install -e '.[latex]'   # antlr4 runtime for math_parse_latex
pip install -e '.[dev]'     # pytest

Lean 4 + Mathlib é instalado por padrão na primeira inicialização do mathkernel-mcp e via mathkernel-lean-setup (elan + um lake workspace fixado). Pule com MATHKERNEL_SKIP_LEAN_INSTALL=1 (CI/wheel smoke).

Nota sobre GPU: As wheels do CuPy não incluem bibliotecas CUDA. O extra cuda instala os pacotes pip nvidia-*-cu12 correspondentes — sem eles, os carregamentos de DLL cuBLAS/NVRTC falham mesmo que import cupy tenha sucesso. A disponibilidade de GPU é verificada em tempo de execução com um matmul real, então uma pilha quebrada degrada graciosamente para CPU. Verifique sua pilha com python scripts/gpu_smoke.py.

Início rápido — servidor MCP

mathkernel-mcp

O servidor fala MCP via stdio (FastMCP 3) e envia instruções principais ao cliente no momento da inicialização: descobrir → analisar → contexto → disciplina de confiança → jobs assíncronos → proveniência. 162 ferramentas, todas prefixadas com math_.

Sessão típica de agente:

math_capabilities                                   # discover surface, limits, engines
math_parse("x^2 - 3*x + 2 = 0")                     # -> expr_id
math_context_create(domains={"x": "real"})          # -> context_id
math_reason(expr_id, context_id, formal=true)       # solve + independently verify
math_derivation_trace(step_id)                      # full provenance on demand

Varreduras de longa duração são assíncronas:

math_job_submit("collatz", {"n_max": 14})  ->  math_job_status(job_id)  ->  math_job_result(job_id)

Início rápido — biblioteca Python

O servidor MCP é uma camada de transporte fina; tudo está disponível in-process:

from mathkernel import MathKernel

kernel = MathKernel()

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

# exact GF(2^m) field arithmetic
f = kernel.gf2m_create(8, "1b")  # AES polynomial x^8 + x^4 + x^3 + x + 1 (hex reduction part)
kernel.gf2m_compute(f.data["field_id"], "mul", ["53", "ca"])

# finite dynamics: an explicit eight-state cyclic permutation
transition = [1, 2, 3, 4, 5, 6, 7, 0]
fs = kernel.finite_system_create("uniform", transition)
km = kernel.koopman_matrix(fs.data["system_id"], {"kind": "walsh", "r": 3})
vis = kernel.koopman_visibility(fs.data["system_id"], {"kind": "walsh", "r": 3})
# Exact zeros certify the requested modes in this declared finite model.

# closure relations (njit meet-in-the-middle)
kernel.closure_search("cyclic", m="97", weight_bound=10, multipliers=["1", "5"])

Módulos independentes (mathkernel.gf2m, mathkernel.koopman, mathkernel.relations, mathkernel.cumulants, mathkernel.finite_fourier, mathkernel.transforms, mathkernel.integral_transforms, mathkernel.complex_analysis, mathkernel.continuous_probability, mathkernel.integers, mathkernel.computational_geometry, mathkernel.algebraic_topology, mathkernel.collatz, mathkernel.cuboid) são utilizáveis sem a fachada quando você não precisa de rastreamento de derivação.

Modelo de confiança

formal                  Lean certificate accepted by the Lean kernel
exact                   exact computation / checked claim-specific certificate
symbolic                symbolic engine agreement (e.g. SymPy residual checks)
interval_certified      rigorous enclosure (mpmath interval)
numeric_high_precision  arbitrary-precision numeric
numeric                 float evidence (incl. GPU fast paths)
empirical / heuristic / unknown

A confiança geral é limitada pela evidência mais fraca necessária para estabelecer o resultado reivindicado — nunca a confiança máxima emitida por qualquer nó individual. A discordância independente entre backends é preservada como um conflito explícito, não calculada como média.

Cada MathResult também carrega um evidence_bundle com evidências separadas de computação, prova, certificado, numérica, de modelo e empírica. claim_evidence retém esses pacotes por conclusão em vez de achatar reivindicações diferentes em um único escore. O campo legado trust permanece um resumo conservador e é automaticamente limitado pela evidência necessária para o resultado. Um justified_trust fornecido pelo produtor é um teto, nunca uma substituição; uma prova ou certificado não verificado suporta apenas unknown.

Status semânticos distinguem a força de prova ou certificação de resultados matemáticos como does_not_exist, undefined, infeasible e unsupported. Essas distinções sobrevivem à serialização MCP, recuperação de jobs assíncronos, reprodução de derivação, visualização e montagem de artefatos multimodais.

O registro de capacidades separa níveis de confiança anunciados de métodos de verificação. Consulte-o por domínio, tipo de entrada/saída, operação, nível de confiança, método de verificação ou mecanismo; registros de capacidade também identificam seu manipulador de execução e dimensões de custo significativas. Planos de expressão registram a rota de capacidade resolvida antes que o executor de obrigações existente a execute.

Caminhos exatos e numéricos são estritamente separados: ferramentas koopman/dinâmica finita usam por padrão exact=true (valores racionais/ciclotômicos de grau de prova); exact=false seleciona o caminho numérico vetorizado (GPU CuPy quando utilizável) e rebaixa a confiança para numeric.

Literais decimais são observações aproximadas. Um decimal (RealNode) em qualquer lugar de uma expressão limita sua confiança a numeric de parse em diante — 0.1 + x é analisado como numeric, 1/2 + x como symbolic. Certificados formais (Lean) e contraexemplos exatos de SMT são recusados para entradas aproximadas, porque os backends codificariam sintaxe decimal como racionais exatos — provando silenciosamente uma afirmação diferente. Use racionais exatos ou certificação por intervalos quando evidência de grau de prova for necessária.

Matemática simbólica contínua

Domínios contínuos usam objetos tipados e o modelo composicional object_create → apply em vez de expor uma superfície CAS plana. Cada operação registra um DAG de quatro obrigações: validação de entrada tipada, cálculo de candidato, verificação de invariante de domínio e reconciliação conservadora de evidências.

• Transformadas integrais — transformadas de Laplace, Fourier, Mellin e Z bilateral com convenções, suposições e regiões de convergência explícitas. A Z inversa usa extração de Laurent/resíduos ciente de anel quando justificada. A verificação registra obrigações de ida e volta, linearidade, convolução, diferenciação, teorema de valor e ROC separadamente; obrigações não resolvidas permanecem unknown.
• Análise complexa — derivadas, candidatos a analiticidade, zeros, singularidades, séries de Laurent, resíduos, integração de contorno, números de enrolamento, contabilidade do princípio do argumento, continuação de identidade conservadora e mapas conformes cientes de domínio. Convenções de ramo, cortes, pontos excluídos, orientação de contorno e incidentes de fronteira permanecem explícitos.
• Probabilidade contínua — distribuições univariadas tipadas, de variável aleatória, conjuntas e condicionais; PDF/CDF/sobrevivência/quantil, momentos, transformadas, entropia, truncamento, convolução, misturas, divergência, marginais, condicionamento/Bayes, covariância/correlação e estatísticas de ordem. Suporte, restrições de parâmetros, Jacobianos e ramos inversos são retidos.

A disponibilidade simbólica é evidência candidata, não prova independente. Identidades do mesmo mecanismo são limitadas a symbolic; ancestralidade decimal permanece limitada a numeric. does_not_exist (por exemplo, uma média de Cauchy) é distinto de um método não suportado ou de uma questão de convergência não resolvida.

Convenções e suposições fazem parte do objeto. Sinal de Fourier e normalização, variáveis de origem/destino da transformada, ramos/cortes complexos, suportes de probabilidade e restrições de parâmetros nunca são selecionados silenciosamente. A orientação de contorno e a contabilidade de singularidades são obrigatórias onde o teorema depende delas.

A verificação é específica da operação. Transformadas retêm cada obrigação de identidade e ROC verificada ou não resolvida. Resíduos são comparados com fórmulas de limite/derivada definidora ou coeficiente de Laurent; reivindicações de contorno retêm singularidades, cortes e números de enrolamento incluídos. Probabilidade verifica normalização, não negatividade ciente de suporte, limites/derivada/monotonicidade de CDF quando decidível, e ramos de Jacobiano. Essas são verificações simbólicas, a menos que um certificado exato ou registro numérico separado diga o contrário.

Falhas usam status semânticos: candidate, unknown, unsupported, does_not_exist e error são distintos. Limitações conhecidas incluem suportes conjuntos não produtivos, continuação sem um domínio de origem sobreposto explícito, entradas sensíveis a ramos do princípio do argumento, transformadas cuja ROC o SymPy não consegue estabelecer, e mudanças multivariadas gerais de variáveis sem ramos inversos/Jacobianos fornecidos.

O trabalho simbólico contínuo é limitado pelos limites globais de AST/saída/tempo de solucionador e limites dedicados de contorno, dimensão conjunta, componente de mistura, ordem de série, estatística de ordem e ramo inverso. Aumente o valor MATHKERNEL_MAX_* correspondente explicitamente quando uma solicitação maior for intencional.

# PDF → Laplace transform, preserving support and evidence ancestry
d = kernel.object_create("Distribution", {
    "family": "exponential", "parameters": ["2"], "variable": "x",
})
r = kernel.apply(d.data["object_id"], "integral_transform", {
    "transform": "laplace",
    "transform_variable": "s",
    "convention": "laplace_standard",
})
assert r.data["value"] == "2/(s + 2)"

Dinâmica finita e análise de PRNG

Uma capacidade distinta: análise espectral exata de sistemas dinâmicos finitos (X, μ, T, O) — construída para (e validada em) análise de estrutura de PRNG.

• Suíte Koopman — matriz de transporte Q, transferência de observação C, visibilidade de modo ρ_O, tensores de estado defasados (brutos/conectados), estatísticas observadas, diagnósticos IPR/entropia. Bases de Walsh para GF(2)^r, bases de caracteres para Z_M.
• Transferência estocástica de observação (API de biblioteca) — contrações exatas FiniteJointLaw para leis conjuntas latentes finitas arbitrárias; momentos/cumulantes ordenados de caminhos Markovianos com os operadores de multiplicação necessários; certificados de defeito de multiplicatividade por estado; e dilatações determinísticas exatas com ruído finito para núcleos Markovianos racionais. O piloto publicado de quartetos de primatas acompanhante registra deliberadamente que o diagnóstico anterior de divisão zero K3ST não sobrevive fora de suas suposições baseadas em grupos.
• Tensores Markovianos gerais ramificados (API de biblioteca) — leis exatas de soma-produto FiniteMarkovTree e cumulantes em árvores enraizadas heterogêneas; certificados exatos de achatamento de arestas L M R com o limite agudo de posto de transição; canais estocásticos locais de observação como transformadas de Kronecker; recuperação exata de inversa à esquerda, testemunhas de colisão, fusão coletiva de sensores e limites de valores singulares condicionados ao canal. O piloto publicado de primatas distingue identificabilidade algébrica de estabilidade de amostra finita.
• Inferência filogenética estatística (API de biblioteca) — projeção no simplex de probabilidade; EM com canal conhecido e recuperação ridge restrita; seleção de regularização por validação retida; covariância multinomial e informação de Fisher no espaço tangente; verossimilhança multinomial de posto não negativo; diagnósticos de posto de Wald por covariância; e pontuação de quartetos segura contra empates. Experimentos controlados GM(4) quantificam a origem compartilhada de valores singulares da perda de visibilidade e da instabilidade inversa. Dois pilotos fixos com dados publicados adicionam verificações de bootstrap por sítio e por bloco móvel sem reivindicar precisão competitiva ampla.
• Benchmarking filogenético congelado (API de biblioteca) — ingestão de FASTA, PHYLIP relaxado, NEXUS prático e Newick; manifestos portáteis SHA-256 de fonte; protocolo canônico e bloqueios de corpus; amostragem de quartetos cega a resultados a partir de divisões de árvore de referência; proveniência de sítios de caso completo; reamostragem de sítios, blocos circulares, estratificada por partição e de partição inteira; linhas de base de cauda de posto, distância p e log-det normalizado; e resumos de corpus seguros contra empates. A execução agrupada avalia 22 unidades correlacionadas pré-declaradas de dois alinhamentos de fonte publicados e uma grade de estresse de verdade conhecida de 1.920 alinhamentos. Um bloqueio separado fixa os primeiros 20 conjuntos de dados elegíveis do BenchmarkAlignments antes da aquisição; esse corpus externo está explicitamente pendente em vez de ser silenciosamente substituído.
• Detecção de relação conectada observável (API de biblioteca) — leis exatas e numéricas de interação pura; espectros singulares de expectativa condicional ponderada; visibilidade estocástica específica de modo; transferência exata de amplitude conectada por canal local; retenção de informação qui-quadrado e Fisher nula; certificados exatos de invisibilidade; limites finitos necessários e construtivos suficientes de amostra; escalonamento de paridade binária; e fusão de sensores complementares. O teorema controlado mostra que perdas locais de visibilidade multiplicam em amplitude e elevam ao quadrado em informação, resultando em uma lei de custo de detecção s^(-2d) na especialização binária homogênea.
• Visibilidade de subespaço de relação e design de sensores (API de biblioteca) — leis de relação locais finitas multiparâmetro; matrizes de Fisher Gram latentes e observadas; autovalores generalizados de informação retida e direções principais de visibilidade; certificados exatos de colisão cegos a observação; multiplicadores de informação e amostra em nível de direção; seleção de subconjunto de sensores por posto, E-ótimo, traço, D-ótimo e pseudo-logdet; transferência empírica eficiente de partição; e correção de média de pontuação por covariância de longo prazo. Um adaptador SkewDB congelado adiciona auditoria de fonte/esquema, divisões de descoberta/validação/desafio por taxonomia retida, pré-processamento apenas de descoberta, hash de fonte e um executor de dados brutos com falha fechada. O fixture SkewDB agrupado é explicitamente sintético porque a carga completa atual não foi adquirida neste ambiente.
• Geometria de relação invariante a coordenadas (API de biblioteca) — vetores tangentes de simplex finito com a métrica de Fisher intrínseca; pushforward tangente estocástico; autovalores generalizados de informação retida invariantes a coordenadas; equivalência exata de pontuação/tangente; transferência exata de qui-quadrado local; limites mínimos de amostra necessários minimax na pior direção; contagens suficientes pontuais finitas de Bhattacharyya e baseadas em retenção; e intervalos de bootstrap iid, de bloco móvel e de cluster para espectros de relação ordenados. Um adaptador SkewDB de resolução local bloqueado por SHA-256 converte faixas cumulativas documentadas *_fit.csv em incrementos de janela e separa explicitamente entradas genuínas do fixture gerado parametrizado por fonte agrupado.
• Fourier finito — aritmética exata em ℚ(ζ_L) via polinômios ciclotômicos: DFT sobre Z_M, transformadas de transferência de saída, coeficientes de diferença de dois pontos, transformadas de Fourier de medida, correções de órbita.
• Busca de fechamento — relações irredutíveis curtas selecionadas pela dinâmica: cíclicas (Σ k_j·a^j ≡ 0 mod m) e binárias (⊕ (L^{jK})ᵀ w_j = 0), meet-in-the-middle com limites de peso L1/Hamming.
• GF(2^m) a partir de transições — reconstruir o corpo (base cíclica de órbita dupla, polinômio mínimo/de redução, verificado por Rabin) puramente a partir das colunas de transição GF(2)-lineares de um gerador.
• Dinâmica condicionada por estado — acesso exato a órbita por estado T^κ(x)(x): resolução de menor defasagem, conversão de simetria para acesso, composição de cociclos, provas exaustivas de fechamento aditivo, mapas de acesso afins simbólicos, resolução de órbita GF(2) baby-step/giant-step, fechamentos preditivos esparsos de defasagem gigante, e descoberta de simetria restrita onde a sondagem numérica apenas classifica candidatos — provas de reescrita canônica ou exaustivas decidem.

A árvore scripts/ contém reproduções uniformes de ponta a ponta para mais de 25 geradores (famílias xorshift/xoroshiro/xoroww, MT19937, Melg19937, WELL19937a, MRG32k3a, PCG32/64(+fast), LXM, SplitMix64, SFC64, JSF64, Romu, Philox, Threefry, RXS-M-XS), cada um executável do zero com scripts/families/run_all.py e scripts/companion/run_all.py. Os dados de referência são fornecidos em scripts/data/ — nenhum fixture externo é necessário.

Matemática de engenharia

O MathKernel fornece matemática de engenharia tipada para sinais, sistemas de controle e otimização com restrições, preservando os mesmos contratos de evidência e persistência do núcleo simbólico.

Sinais e espectros

Sinais contínuos e amostrados carregam domínios explícitos, grades de amostragem e unidades. Representações espectrais são tipadas em vez de tratadas como matrizes anônimas. Filtros FIR/IIR e projetos de filtro retêm coeficientes, convenções e sinais de origem, enquanto o estado de streaming imutável torna o processamento bloco a bloco reproduzível. Operações de resposta em frequência e tempo registram se usaram álgebra simbólica exata ou avaliação numérica.

Sistemas de controle

Modelos SISO e MIMO tipados suportam representações em espaço de estados e função de transferência, conversão contínuo/discreto, polos e zeros, verificações de estabilidade, discretização, construção de controladores e construção de observadores. LQR, LQR de horizonte finito, filtragem de Kalman em estado estacionário, composição LQG e estados imutáveis de predição/atualização de Kalman retêm ancestralidade de planta/modelo e separam verificações algébricas de suposições de modelagem.

MPC de horizonte finito com restrições mantém separadas as afirmações de viabilidade, otimalidade, invariância terminal, viabilidade recursiva e estabilidade. Análise no domínio da frequência inclui representações de Bode, Nyquist e lugar das raízes juntamente com respostas temporais verificadas.

Otimização e certificados

Programas lineares e quadráticos podem retornar testemunhas exatas/verificáveis de otimalidade onde o fragmento suportado permite. LPs inviáveis podem expor certificados de Farkas e problemas ilimitados podem expor raios de recessão. Resultados de busca MILP carregam árvores de prova reproduzíveis em vez de apenas um valor incumbente. Fluxos de trabalho cônicos e com restrições quadráticas suportam cones de produto SOCP/SDP limitados e certificados estilo Lagrangeano em seus fragmentos declarados.

Solucionadores candidatos nativos externos são isolados em processos novos com solicitações limitadas e término por tempo limite rígido. A geração de candidatos e a verificação de certificados são etapas distintas: um solucionador que encontra um ponto não estabelece por si só uma afirmação mais forte do que o verificador pode checar.

Geometria e topologia

Geometria diferencial e cálculo tensorial

Objetos imutáveis Manifold, Chart e Metric alimentam saídas tipadas GeometryTensor, Connection e GeodesicSystem. Operações métricas calculam métricas inversas, símbolos de Christoffel, curvatura de Riemann/Ricci/escalar/Einstein e equações geodésicas afins. Verificações simbólicas exatas cobrem identidades inversas, liberdade de torção, compatibilidade métrica, simetrias de Riemann, a primeira identidade de Bianchi e a identidade de Bianchi contraída. Domínios de carta e condições de não degenerescência métrica permanecem explícitos.

Objetos direcionais CoordinateMap carregam Jacobianos explícitos e verificações de composição inversa. Objetos densos TensorField cientes de variância e objetos esparsos canônicos DifferentialForm suportam derivadas covariantes e de Lie, produtos wedge, derivadas exteriores, produtos interiores, pullbacks e estrelas de Hodge. Verificações incluem comutatividade graduada, d²=0, comutação de pullback com d, compatibilidade métrica, composição de mapas de coordenadas e o sinal de dupla estrela de Hodge quando a assinatura métrica é fornecida. Orientação e assinatura nunca são adivinhadas.

Geometria computacional

Objetos Point, PointSet, Polygon, de semiespaço Polytope, Triangulation e derivados VoronoiDiagram fornecem predicados exatos de orientação, incírculo e interseção de segmentos, envoltórias convexas por cadeia monotônica, contenção por enrolamento, vizinhos mais próximos exatos por distância ao quadrado, recorte de orelhas certificado, recorte de polígonos convexos, triangulação de Delaunay com circuncírculo vazio e duais de Voronoi finitos com raios ilimitados explícitos. Predicados decimais usam filtros conservadores de erro de ponto flutuante; quando a topologia não pode ser estabelecida, o resultado é explicitamente ambíguo em vez de promovido a uma classificação exata.

Topologia algébrica

Objetos exatos finitos SimplicialComplex, CubicalComplex e integrais ChainComplex expandem células para fechamentos de face canônicos e derivam matrizes de fronteira orientadas. Complexos verificam boundary[k-1] * boundary[k] = 0 antes que a homologia seja tentada. homology calcula postos livres e torção inteira sobre Z por meio de reduções certificadas de núcleo/quociente de Smith, e números de Betti exatos mais ciclos representativos sobre Q ou GF(p). boundary_matrix, chain_complex e euler_characteristic expõem bases ordenadas e a verificação cruzada de Euler–Poincaré.

Triangulações exatas verificadas podem ser convertidas em complexos simpliciais canônicos e compostas diretamente com operações de homologia; triangulações numéricas ou refutadas não podem cruzar essa fronteira de exatidão. A expansão de fechamento é limitada antes que o crescimento combinatório possa exceder os limites de topologia configurados. Homologia persistente, produtos de cohomologia e inferência de complexos infinitos/CW não são reivindicados.

Estatística e modelagem estocástica

Amostras e estatísticas descritivas

StatisticalSample armazena uma matriz retangular não vazia de observações reais concretas finitas, rótulos de variáveis únicos, IDs de observação opcionais únicos e metadados explícitos de amostragem/população/design. describe deriva momentos numéricos exatos ou limitados por ancestralidade e estatísticas de ordem tipo 7; covariance deriva produtos cruzados centrados com normalização de amostra ou população; empirical_distribution preserva contagens de frequência exatas e probabilidades racionais; e evidence_profile audita a própria fronteira de evidência. A evidência exigida estabelece apenas cálculos sobre as observações armazenadas. Metadados de amostragem, suporte empírico e suposições de modelo permanecem em registros separados de evidência diagnóstica, enquanto generalização populacional e validade do modelo permanecem explicitamente não estabelecidas. Valores ausentes, observações simbólicas não resolvidas e imputação silenciosa são recusados. Entrada decimal não pode ser promovida, limites de recursos são verificados antes de trabalho caro, e todo objeto derivado mantém sua origem através de persistência e reinicialização.

Modelos lineares generalizados

Objetos imutáveis GeneralizedLinearModel vinculam-se a amostras armazenadas e produzem objetos GLMFit apenas derivados. Pares canônicos suportados são Gaussiano/identidade, binomial/logito e Poisson/log. verify verifica domínio da resposta, posto do delineamento e graus de liberdade residuais; fit relata coeficientes ordenados, covariância/erros padrão, médias condicionais ajustadas, desvio, desvio nulo, dispersão, convergência, resíduo de escore e condicionamento. Ajustes suportam independentemente verify, diagnostics e predict.

Modelos gaussianos de entrada exata usam produtos cruzados suficientes e equações normais exatas. Ajustes gaussianos numéricos usam mínimos quadrados float64 verificados; ajustes logísticos e de Poisson usam IRLS float64 determinístico. Deficiência de posto, domínios de resposta inválidos ou degenerados, não convergência, informação singular/mal condicionada e separação completa/quase detectada falham de forma fechada sem objeto de ajuste. Nenhum termo de crista, exclusão de linhas, imputação ou substituição de família/ligação é silencioso. Coeficiente, covariância, desvio e alegações de previsão permanecem condicionais à amostra/delineamento armazenados; validade do modelo, generalização populacional e efeitos causais não são inferidos.

Testes não paramétricos, testes de permutação e bootstrap

Amostras armazenadas suportam mann_whitney, wilcoxon, kruskal_wallis, ks_2samp, spearman e kendall, com postos médios explícitos e correções de empate. method="auto" realiza enumeração completa exata de sinais/rótulos/permutações somente quando tanto o estado quanto as estimativas de trabalho se ajustam aos limites configurados; caso contrário, o resultado nomeia sua aproximação normal, qui-quadrado, Kolmogorov ou t de Student. Assim, um valor-p exato é um cálculo nulo condicional exato para as observações armazenadas, enquanto um valor-p assintótico permanece evidência numérica sem teorema de erro de amostra finita.

permutation_test suporta diferenças de média/mediana usando enumeração exata ou Monte Carlo PCG64 explicitamente semeado com valor-p aditivo. bootstrap suporta intervalos percentílicos de média/mediana com semente uint64 obrigatória, sorteios limitados e lotes com memória limitada. Resultados simulados registram algoritmo aleatório, semente, contagem de sorteios e configuração de reprodução. Trocabilidade, delineamento amostral, validade assintótica, cobertura populacional e interpretação causal permanecem suposições separadas ou alegações não estabelecidas.

Análise de sobrevivência

SurvivalDataset armazena durações, indicadores binários exatos de eventos, tempos opcionais de entrada tardia e estratos opcionais dentro de uma amostra estatística imutável. kaplan_meier constrói conjuntos de risco exatos e valores de produto-limite juntamente com erros padrão numéricos de Greenwood e intervalos log-log bilaterais. Entradas multiestrato exigem um estrato explícito, e survival_at consulta a curva de degraus contínua à direita.

CoxProportionalHazardsModel fornece uma superfície de Cox não estratificada com laços explícitos de Efron ou Breslow. Seu ajuste Newton float64 determinístico usa busca de linha monotônica e recusa casos com deficiência de posto, eventos esparsos, não convergentes, singulares, supercondicionados ou semelhantes a separação. CoxPHFit registra coeficientes/razões de risco, covariância/erros padrão, verossimilhança parcial, resíduo de escore, risco basal, concordância e correlações temporais de Schoenfeld, com verificação de reprodução, diagnósticos e previsão de risco parcial limitada. Censura independente, riscos proporcionais, generalização populacional e causalidade permanecem suposições ou não estabelecidas.

Modelos de séries temporais e previsão

TimeSeriesDataset preserva ordem das linhas, colunas distintas de tempo/valor, carimbos de tempo estritos, política de rejeição de ausentes e espaçamento regular detectado. acf de origem exata usa um denominador centrado comum com defasagem zero e pacf usa recursão de Durbin–Levinson. stationarity_test fornece uma regressão ADF numérica de caso constante com valores críticos assintóticos nomeados em vez de inventar um valor-p exato ou afirmar que estacionariedade é provada.

TimeSeriesModel cobre ordens AR, MA, ARMA, ARIMA e GARCH, escolha de constante, inovações gaussianas e inicialização. Ajustes da família ARMA usam otimização limitada de soma condicional de quadrados; GARCH usa verossimilhança gaussiana restrita com variância positiva e persistência abaixo de um. Ajustes derivados registram coeficientes, séries residuais/ajustadas, variância condicional, raízes, verossimilhança, AIC/BIC e convergência, com diagnósticos de Ljung–Box/Jarque–Bera. Previsões derivam tempos futuros regulares, médias recursivas e intervalos gaussianos usando respostas de impulso ARIMA ou recursão de variância GARCH. Espaçamento irregular pode ser analisado, mas não ajustado.

Processos estocásticos

Objetos imutáveis PoissonProcess, WienerProcess, GaussianProcess e ContinuousTimeMarkovChain expõem leis de dimensão finita e artefatos derivados verificados. Massas/momentos de contagem de Poisson e médias/covariâncias de Wiener são simbólicos ou exatos. Leis finitas de processos gaussianos suportam núcleos RBF, Matérn-3/2, linear e Browniano com verificações numéricas de PSD; condicionamento usa soluções de Cholesky float64 limitadas, variância explícita de ruído de observação e jitter armazenado opcional sem ajustar hiperparâmetros silenciosamente. Verificação de CTMC verifica axiomas de gerador e lei inicial exatamente; transições usam exponencial de matriz verificada, enquanto leis estacionárias usam um sistema exato de espaço nulo esquerdo e preservam não unicidade.

Incrementos independentes/estacionários, continuidade, gaussianidade, adequação do núcleo e homogeneidade temporal permanecem suposições de modelo declaradas, não fatos estabelecidos por cálculo.

Equações diferenciais estocásticas

StochasticDifferentialEquation suporta sistemas de Itô vetoriais com escopo de símbolo declarado, vetor de deriva, matriz de difusão completa estado-por-ruído, estado inicial concreto e intervalo finito. Euler–Maruyama suporta estados vetoriais e difusão completa. Milstein é restrito a estado escalar/ruído escalar e usa a derivada simbólica da difusão; casos multidimensionais não suportados são recusados em vez de substituir silenciosamente outro esquema.

Simulação registra a grade de passos exata quando possível, caminhos float64, algoritmo/semente/fluxo PCG64, momentos amostrais terminais e ordens nominais forte/fraca. Saídas grandes expõem metadados compactos mais consultas limitadas de caminho/terminal. Estudos de convergência acoplados reutilizam um fluxo Browniano mais fino em múltiplos tamanhos de passo e relatam convergência RMS terminal observada quando definida. Simulação e convergência permanecem numéricas/empíricas; ordens nominais, existência, unicidade e regularidade são suposições, não provas.

Evidência estatística e persistência

Em todos os objetos estatísticos/estocásticos, evidência exata, simbólica, assintótica, numérica, empírica e de modelo permanecem distintas. Tipos derivados são somente saída, reprodução opera sob limites atuais, ancestralidade decimal não pode ser promovida, JSON persistido é verificado quanto à integridade antes da decodificação, e campos armazenados de tipo/classe/origem são reconciliados para prevenir substituição de origem entre tipos.

EDPs e elementos finitos adaptativos

Representação e classificação de EDPs

Problemas de EDP tipados suportam sistemas escalares e acoplados, variáveis independentes/dependentes declaradas, multi-índices de derivadas, coeficientes/parâmetros e condições iniciais/de contorno explícitas. Análise de parte principal classifica o sistema representado somente dentro do fragmento simbólico declarado, e verificações de compatibilidade de traço distinguem informação de contorno representada de alegações mais fortes como existência, unicidade, regularidade ou boa colocação.

Formas fracas

Artefatos PDEFunctionSpace, PDEMeasure, WeakIntegralTerm, IntegrationByPartsStep e somente saída WeakForm representam formulações fracas explicitamente. derive_weak_form exige variáveis de integração, espaços de tentativa ordenados, espaços de teste, índices de traço de contorno e transferências selecionadas de termo/coordenada; não adivinha espaços analíticos nem integra termos silenciosamente.

Integração por partes com coeficiente variável retém a regra do produto completa, armazenando termos de volume com teste diferenciado e derivada de coeficiente separadamente. Cada transferência emite faces de contorno orientadas. Termos de contorno que desaparecem sob traços de teste zero declarados permanecem representados e são marcados como tais. Índices de Dirichlet, Neumann/Robin e periódicos são registrados como partições essenciais, naturais e periódicas. WeakForm.verify reconstrói espaços, medidas, termos de volume/contorno, sinais, derivadas da regra do produto, partições e etapas de derivação a partir da EDP de origem. A alegação verificada é a identidade integral representada sob suposições declaradas—não um teorema de solubilidade ou regularidade.

Malhas, elementos de referência e espaços de elementos finitos

FEMMesh suporta simplexos de intervalo, triângulo e tetraedro. Construção verifica conectividade limitada, não degenerescência, orientação positiva canônica, incidência de facetas de contorno/interior, propriedade de contorno induzida e componentes conexas de células. Um Triangulation armazenado compatível pode fornecer conectividade de triângulo preservando geometria e ancestralidade de forma fraca. Reprodução combinatória não infere não sobreposição geométrica ou qualidade de aproximação.

reference_element fornece simplexos unitários canônicos. basis deriva funções e gradientes de Lagrange P1 nodais simbólicos e verifica a propriedade de Kronecker, partição da unidade e soma de gradientes. quadrature fornece regras de momento exato limitadas para os graus de simplex suportados. finite_element_space constrói espaços C0 de vértice-DOF P1 com conectividade local-para-global explícita e DOFs de contorno essenciais. Objetos derivados são reproduzíveis e somente saída.

Montagem e soluções algébricas

AssembledSystem e FEMSolution suportam formas fracas estacionárias lineares escalares em simplexos P1 afins. Montagem armazena matrizes/vetores locais densos e determinantes jacobianos, coalesce a matriz global em entradas esparsas ordenadas, integra termos de faceta de Neumann/Robin suportados e realiza eliminação simétrica documentada para DOFs de Dirichlet retendo sistemas brutos e transformados. Substituições concretas resolvem parâmetros restantes de EDP através de MathIR restrito.

Montagem distingue integração exata de uma soma de quadratura finita exata. Quadratura de ordem insuficiente ou não polinomial pode ainda definir um sistema algébrico reproduzível, mas quadrature_exact=false registra a limitação. Segundas derivadas fortes não suportadas, derivadas temporais, campos acoplados/não lineares, restrições periódicas, parâmetros não resolvidos e fluxos de contorno ausentes falham de forma fechada.

Soluções selecionam análise exata de posto/posto aumentado ou um caminho numérico esparso explícito do SciPy. FEMSolution registra unique, ill_conditioned, singular_inconsistent, singular_underdetermined ou singular_least_squares, juntamente com resíduo e diagnósticos de condicionamento. Verificação estabelece o sistema de dimensão finita transformado e o resultado do solucionador somente, nunca um teorema de solução contínua de EDP ou limite de erro contínuo.

Estimativa de erro e adaptatividade

FEMSolution.estimate_error fornece indicadores de resíduo–salto para soluções P1 completas únicas ou mal condicionadas em seu fragmento de difusão estacionária escalar suportado. Cada CellErrorIndicator retém resíduo forte ponderado por diâmetro, contribuição de salto conormal interior, contribuição de contorno natural e total. FEMErrorEstimate armazena valores de estimador local/global, exatidão de quadratura e resíduo algébrico separadamente, e sempre registra rigorous_error_bound=false; constantes de confiabilidade e eficiência não são inferidas. FEMErrorEstimate.mark implementa políticas determinísticas de Dörfler e de máximo. RefinementMarking.refine aplica o refinamento vermelho de triângulos e propaga o fechamento conforme através de arestas compartilhadas. RefinedMesh registra células solicitadas/de fechamento e mapeamentos filho-pai; MeshTransfer registra valores nodais P1 refinados como combinações afins explícitas de DOFs pais. Malhas refinadas podem reentrar na cadeia de base, quadratura, espaço, montagem, solução e estimação.

FEMErrorEstimate.compare aceita pares diretos de refinamento pai/filho e relata razões de estimadores e taxas observadas de duas malhas. FEMConvergenceObservation é evidência explicitamente empírica sobre uma sequência de estimadores, não um teorema de convergência ou limite de erro contínuo.

Inferência de relações e geometria da informação

Inferência composta de relações

mathkernel.composite_relation_inference fornece um teste de escore quadrático para um subespaço inteiro de relações visíveis. Escores observados generalizados são branqueados sob a lei nominal e a estatística é a norma quadrada de sua média amostral. Um argumento finito de escore limitado fornece uma garantia conservadora com dependência explícita da dimensão da relação, do menor autovalor de informação retido, do raio de perturbação e do limite do escore.

O mesmo módulo calcula informação alvo ajustada por incômodo através de complementos de Schur de Fisher latentes e observados. Ele relata confusão exata pós-observação quando uma direção alvo pode ser reproduzida por variação de incômodo. Para autovalores de informação repetidos ou quase repetidos, a incerteza bootstrap é anexada a autoespaços invariantes através de ângulos principais, em vez de autovetores individuais arbitrários. Intervalos de espectro ordenado studentizados, heurísticas de blocos circulares informadas por dependência, modos de covariância nominal/empírico/HAC e garantias de especificação incorreta limitadas por norma estão disponíveis com suas suposições registradas.

Inferência robusta de relações

mathkernel.robust_relation_inference fornece inferência quadrática com escopo de modelo, projeções de incômodo aprendidas, relações residuais ortogonais e estimação de covariância de longo prazo pré-branqueada por VAR.

API Python	Função e limite de evidência
quadratic_minimax_bounds	Taxas inferior/superior de sequência gaussiana usando o espectro de informação inverso; limite separado finito iid de estatística U sob um envelope de covariância justificado
gaussian_quadratic_test	Teste de quadrado ponderado com limiar finito de Chernoff gaussiano
quadratic_u_test	Estatística de par não enviesada O(Nr); calibração finita de Cantelli para escores iid de nulo conhecido
prewhitened_long_run_covariance	VAR(1), largura de banda automática de Bartlett, recoloração e diagnósticos de persistência; suposições de consistência permanecem necessárias
quadratic_moment_test	Teste de Wald assintótico de posto completo com covariância empírica ou fornecida; covariância singular é rejeitada
relation_folds	Dobras iid reproduzíveis, preservadoras de grupo ou contíguas
crossfit_nuisance_projection	Estimação de projeção de incômodo fora da dobra em um intervalo candidato declarado
crossfit_residual_relations	Momentos cruzados residuais ortogonais com médias condicionais aprendidas, aprendizes personalizados e lacunas de exclusão

Essas APIs de pesquisa permanecem numéricas/com escopo de modelo, a menos que uma garantia finita mais forte seja explicitamente retornada. Elas não adquirem rótulos de prova formal ou certificação de intervalo meramente por serem compostas com outros objetos MathKernel.

Visibilidade de relações, design de sensores e geometria da informação

A pilha de análise de relações também inclui visibilidade exata de relações observáveis, cálculos de retenção de informação, diagnósticos de custo amostral, geometria de Fisher multi-relação, objetivos de design de sensores, representações tangentes invariantes a coordenadas, limites de teste locais e incerteza para espectros de informação. Direções numéricas quase nulas são mantidas distintas de direções cegas matematicamente exatas.

Desempenho: numba · CUDA · paralelismo

Carga de trabalho	Caminho rápido de CPU	Caminho de GPU	Paralelo
Peneira de Collatz	njit (n ≤ 31)	CUDA RawKernel	pool de processos persistente
Varredura de cuboide	njit varredura de pares de pernas + pré-filtro QR	CUDA RawKernel	pool de processos
GF(2^m) ≤ 1024	njit kernels de n-limb (uint64×N)	—	—
Lote inteiro	njit kernels de array	—	pool de processos persistente, tamanho de chunk adaptativo
BFS/componentes de grafo	njit travessia CSR, certificado re-verificado	—	—
GF(p^m), p < 2^24, m ≤ 64	njit multiplicação/mod polinomial uint64	—	—
Validação de tabela de Cayley	njit varredura de axiomas	—	—
Extensão de recorrência	njit int64 verificado, fallback bigint	—	—
FWHT	njit borboleta int64	—	—
Busca de fechamento	njit MITM (int64/uint64)	—	—
Dinâmica de Koopman / finita	numpy complex128	CuPy matmul	—
DAG de obrigações	—	—	ondas de threads
Varreduras longas	—	—	pool de jobs assíncrono

Tipos simbólicos exatos (Fraction, CyclotomicNumber) são deliberadamente Python puro — uma visibilidade zero ou cancelamento de fechamento deve permanecer uma prova. Gêmeos numéricos existem onde a escala exige e sempre carregam trust: numeric.

Contrato de expansão. Novos domínios devem projetar verificação e camadas de desempenho juntas desde o início: semântica tipada exata e limites, um certificado verificável independentemente para cada reivindicação VERIFIED e — onde a carga de trabalho é regular o suficiente — um caminho rápido Numba/processo/GPU atrás de um fragmento de exatidão estreito com fallback automático em Python. Caminhos rápidos devem ser re-verificados ou testados diferencialmente contra a implementação de referência e devem registrar o backend selecionado nos metadados de evidência; eles nunca podem elevar a confiança além da prova subjacente. Descarregamento de GPU é obrigatório apenas para cargas de trabalho regulares exatas por dispositivo; algoritmos irregulares de precisão arbitrária documentam as camadas consideradas em vez disso.

Otimização que preserva a correção

MathKernel otimiza apenas onde o contrato matemático sobrevive à otimização. Cargas de trabalho regulares limitadas de inteiros/arrays usam caminhos Numba, processo ou GPU com verificações diferenciais e fallbacks protegidos. Cargas de trabalho simbólicas exatas permanecem em representações exatas quando convertê-las para ponto flutuante enfraqueceria a reivindicação. A criação de perfil é usada para remover trabalho simbólico repetido, elevar computações invariantes, armazenar em cache certificados reproduzíveis e substituir passagens de verificação superlineares evitáveis sem alterar evidência matemática armazenada. A seleção de backend é registrada nos metadados de evidência e nunca eleva a confiança acima da computação ou certificado subjacente.

Visualização e artefatos portáteis

mathkernel_viz transforma objetos e resultados MathKernel em artefatos interativos que carregam evidência. A visualização é a jusante da matemática: ela consome dados de origem tipados ou um MultimodalProjection, registra transformações de apresentação e nunca atualiza a evidência de origem meramente porque uma forma gráfica particular é usada.

import mathkernel_projection as mkp
import mathkernel_viz as viz

projection = mkp.create_projection(
    "matrix",
    {"matrix": [[1, 2], [3, 4]]},
    trust="exact",
)
doc = viz.from_projection(projection)
viz.export_html(doc, "matrix.html", mode="portable")

A API de dashboard de nível inferior permanece disponível para composição direta:

import mathkernel_viz as viz

doc = viz.dashboard("My result", cols=2)
viz.add_point_cloud(doc, points, trust="numeric")
viz.add_histogram(doc, values, bins=128)
viz.add_select(doc, "lag", [
    {"label": "k=4", "value": {"embed": {"lags": [0, 4, 8]}}}
])
viz.export_html(doc, "out.html", mode="portable")

• Blocos de construção, não monólitos — artefatos compõem painéis reutilizáveis como point_cloud_3d, trajectory_3d, surface_3d, vector_field_3d, plot2d, histogram, heatmap, dag, metric_grid, data_table, text e select.
• IR neutro de renderizador — o VisualizationDocument versionado é consumido por SVG puro em Python, matplotlib PNG/PDF opcional e o renderizador HTML+Three.js.
• 3D interativo — órbita/pan/zoom e inspeção por hover de identidade e confiança.
• HTML portátil — um .html autocontido com conjuntos de dados embutidos, proveniência, metadados de reprodutibilidade e runtime de visualizador; nenhum servidor ou CDN é necessário.
• Preservador de evidência — a confiança de bloco/série/conjunto de dados é herdada conservadoramente; exibição certificada por intervalo é usada apenas quando a própria fonte carrega esse suporte.
• Integridade e determinismo — SHA-256 de payload e por conjunto de dados são expostos, e entradas idênticas produzem artefatos determinísticos.
• Limite de apresentação seguro — CSP, rótulos escapados, sem eval, limites de conjunto de dados, e MathIR tratado como dados em vez de código executável.

Projeções multimodais compartilhadas

A camada compartilhada mathkernel_projection define famílias canônicas de projeção matemática que podem alimentar visualização, sonificação ou um artefato de pesquisa combinado. Isso impede que cada renderizador invente sua própria interpretação de uma matriz, malha, grafo, campo, distribuição ou objeto de alta dimensão.

Um MultimodalProjection registra:

• linhagem de origem (SourceRef);
• família de projeção e payload estruturado;
• coordenadas, unidades e rótulos;
• suposições e referências de evidência;
• proveniência de transformação determinística;
• parâmetros explícitos de base, fatia, travessia ou ordenação;
• dimensionalidade de saída e perda de informação declarada.

As famílias canônicas cobrem campos escalares/vetoriais; conjuntos de pontos/nuvens; curvas, superfícies e trajetórias; sequências e distribuições; matrizes e tensores; grafos, grafos de evidência, árvores de expressão e árvores de certificado; espectros e campos de valor complexo; regiões e conjuntos implícitos; malhas e complexos geométricos; soluções de ODE/PDE e sistemas dinâmicos; objetos de otimização e inferência estatística; estruturas de campo finito/GF(2); geometria de relação/informação; conjuntos, partições e objetos por partes; quantidades com unidades; ensembles; e projeções explícitas de alta dimensão.

Para dimensão de origem maior que três, um método de projeção e dimensionalidade de saída devem ser explícitos. Seleção de coordenadas, uma base declarada, redução tipo PCA ou uma projeção espectral específica de domínio são transformações que devem ser registradas; um renderizador não pode decidir silenciosamente qual visão é canônica.

Um registro de adaptadores de resultado (mathkernel_projection.result_adapters) mapeia objetos tipados armazenados e payloads de resultado planos para essas famílias automaticamente. Adaptadores são funções puras de extração: eles nunca recomputam matemática, nunca atualizam confiança e declaram qualquer escolha de apresentação (grades de amostragem, espectros somente de magnitude, seleção de canal, redução covariância-para-banda) em parameters e information_loss. math_visualize(object_id=...) e math_projection_create(source_object_id=...) usam o registro para escolher a projeção canônica para sinais, espectros, filtros, mapas polo-zero, respostas de frequência, lugares de raízes, respostas de tempo, distribuições (densidades simbólicas são amostradas em uma janela declarada), distribuições empíricas/discretas, amostras estatísticas, ajustes GLM, estimativas de Kaplan-Meier, riscos de base de Cox, diagnósticos ACF/PACF, ajustes de séries temporais, grafos e árvores de travessia, resultados de otimização, ensembles ODE/SDE, malhas/soluções/indicadores de erro/observações de convergência FEM, padrões de esparsidade de sistemas montados, grades de PDE, conjuntos de pontos, polígonos, triangulações, diagramas de Voronoi, funções geradoras, tabelas de Cayley, contornos, mapas de singularidade, partições de subgrupo/cossete/órbita, contagens combinatórias e quantidades com unidades. Tipos de objetos não registrados falham com um erro tipado em vez de uma visão inventada.

Grafos de evidência são cidadãos de primeira classe: relações reivindicação -> evidência -> suposição/origem podem ser visualizadas diretamente, tornando a estrutura de verificação do MathKernel inspecionável em vez de escondê-la em metadados. Projeções de valor complexo retêm estrutura de magnitude/fase, e projeções de malha/campo preservam a entidade geométrica à qual cada valor pertence.

Linhagem de artefatos e apresentação científica

mathkernel_viz, mathkernel_sonify e mathkernel_multimodal compartilham a camada semântica mathkernel_artifacts. MathKernelArtifact carrega linhagem de origem tipada, evidência/certificados, transformações de apresentação, anotações científicas/perceptuais, metadados de reprodutibilidade e sincronização visual/áudio. mathkernel_viz.visualize(result) anexa linhagem estruturada determinística a conjuntos de dados e séries visuais, enquanto mathkernel_viz.to_artifact(doc, result=...) promove um documento visual para o mesmo modelo de artefato que carrega evidência usado por exportações multimodais. A apresentação permanece a jusante da matemática e não pode atualizar a confiança da origem.

Sonificação científica (mathkernel-sonify)

mathkernel_sonify é o irmão auditivo de mathkernel_viz. Ele consome a mesma linhagem de fonte e o contrato MultimodalProjection, enquanto SonificationDocument é responsável pelo mapeamento auditivo em si. O resultado matemático permanece intocado.

import mathkernel_projection as mkp
import mathkernel_sonify as son

projection = mkp.create_projection(
    "spectrum",
    {"amplitudes": [1.0, 0.42, 0.17], "phases": [0.0, 0.3, -0.2]},
    trust="numeric",
)
audio = son.projection_sonification(projection)
son.write_wav(audio, "spectrum.wav")
son.export_html(audio, "spectrum.html")

O IR registra cada mapeamento valor-para-áudio como proveniência declarativa. Objetos estruturados nunca são silenciosamente achatados: varreduras de matrizes registram a ordem linha/coluna; sonificação de tensores registra a fatia/ordem selecionada; grafos registram redução de travessia ou grau; malhas registram a redução geométrica; objetos complexos preservam o mapeamento de magnitude e fase; rastreamentos de otimização, distribuições bootstrap/nulas, espectros de relação e ordenações de ensemble são igualmente explícitos.

Adaptadores integrados cobrem síntese aditiva harmônica/Fourier, varreduras sequenciais, comparação estéreo previsão-vs-observação, sonificação de resíduos e mapeamentos estruturados conscientes de projeção. A renderização offline PCM/WAV é determinística, rejeita aliasing Nyquist silencioso e aplica limites explícitos de normalização/pico. O exportador WebAudio é um único arquivo HTML offline sem dependência de rede.

Regra científica: um padrão audível é um candidato perceptual, não evidência matemática. Qualquer padrão descoberto pela audição deve ser validado quantitativamente, exatamente, formalmente ou empiricamente por meio do MathKernel.

Artefatos multimodais unificados (mathkernel-multimodal)

mathkernel_multimodal combina visualização e sonificação derivadas da mesma fonte/projeção em um único MathKernelArtifact portátil. A ancestralidade compartilhada SourceRef permite sincronização automática entre modalidades sem enfraquecer o modelo de confiança matemática.

import mathkernel_multimodal as mkm

artifact = mkm.build_artifact(
    title="Result",
    visualizations=[viz_doc],
    sonifications=[son_doc],
    mathkernel_version="current",
)
mkm.export_html(artifact, "result.html")

• blocos visuais podem ser destacados durante a reprodução de áudio vinculada e o áudio vinculado pode buscar a partir de um bloco visual;
• uma única superfície de inspeção expõe Resultado, Evidência, Proveniência, Dados, Reprodução, Mapeamento Visual, Mapeamento de Áudio, Sincronização e Anotações;
• verificação de carga útil e hashes de integridade do documento permanecem disponíveis no artefato exportado;
• a saída portátil funciona a partir de file://, sem exigir um servidor MathKernel em execução;
• a confiança do artefato permanece como a confiança de fonte/membro justificada mais fraca.

Via MCP, artefatos de pesquisa podem ser montados a partir de objetos de visualização e sonificação armazenados e exportados como um único arquivo autocontido.

MathKernel Studio

MathKernel Studio é um workbench local opcional baseado em navegador no branch de desenvolvimento Studio. O alpha 0.4 fornece autoria de canvas/contorno, entradas de valores exatos, recuperação, inspeção de evidências, visualizadores isolados de plot/áudio e execução real de fluxo de trabalho local por meio do backend separado mathkernel_workflow.

O backend valida e congela grafos suportados, apresenta planos imutáveis, aplica política de operador e aprovação vinculada à sessão, e supervisiona processos de trabalho do kernel. Solicitações duráveis e snapshots de resultados sobrevivem a desconexões do navegador; processos de host interrompidos nunca são reproduzidos automaticamente. Quinze adaptadores simbólicos/matriciais explícitos e subfluxos de trabalho autocontidos salvos são suportados. Entradas parciais de catálogo legado e destinos não suportados permanecem limitados por capacidade. Rótulos de resultados importados permanecem não confiáveis; a evidência do kernel é preservada.

O wheel opcional do Studio agrupa seus ativos; Node/npm são apenas ferramentas de tempo de compilação. O pacote Python/MCP não importa o Studio. Este é um alpha de execução local testado; a qualificação completa de navegador/acessibilidade/plataforma permanece pendente.

Consulte o guia do Studio para instalação, teclado e edição sem arrastar, a conexão de loopback protegida, publicação de resultados e limites de suporte atuais.

Superfície de ferramentas MCP

Todas as 167 ferramentas (clique para expandir)

Grupo	Ferramentas
Descoberta	math_capabilities, math_capability_query, math_result_resource_get
Matemática tipada	math_object_create, math_object_get, math_apply — superfície composicional completa tabulada acima, incluindo geometria, sinais/controle, otimização certificada, estatística/sistemas estocásticos e representação geral de EDP
Análise	math_parse, math_parse_latex, math_get, math_substitute, math_infer_structure
Álgebra	math_simplify, math_solve, math_solve_system
Cálculo	math_differentiate, math_integrate, math_limit, math_series, math_summation, math_product
Numérico	math_numeric_evaluate, math_interval_evaluate
Matrizes	math_matrix_create, math_matrix_get, math_matrix_det, math_matrix_inverse, math_matrix_transpose, math_matrix_multiply, math_matrix_rank, math_matrix_rref, math_matrix_eigenvalues, math_matrix_solve
Contexto	math_context_create, math_context_infer, math_context_check
Raciocínio	math_analyze, math_plan, math_plan_get, math_execute_plan, math_reason, math_execution_get, math_prove_equivalence, math_counterexample
Geração de código	math_codegen, math_verify_code, math_execute_code
Inteiros	math_integer_analyze, math_integer_compute, math_integer_batch
Varreduras	math_collatz_sieve, math_cuboid_sweep
Tarefas	math_job_submit, math_job_status, math_job_result, math_job_list
GF(2^m)	math_gf2m_create, math_gf2m_from_transition, math_gf2m_compute, math_gf2m_coords, math_gf2m_root_jump_rows, math_gf2m_closure_roots, math_gf2m_jump_rows
GF(2)	math_gf2_rank, math_gf2_nullspace, math_gf2_carryfree_cols, math_gf2_minpoly
Transformadas	math_fwht
Dinâmica finita	math_finite_system_create, math_koopman_matrix, math_koopman_transfer, math_koopman_visibility, math_koopman_lagged, math_koopman_observed, math_koopman_diagnostics, math_finite_fourier_compute, math_closure_search, math_cumulant_compute
Dinâmica condicionada	math_conditioned_access_solve, math_conditioned_symmetry_access, math_conditioned_access_compose, math_conditioned_closure, math_symbolic_conditioned_access, math_affine_conditioned_access, math_gf2_conditioned_access, math_gf2_predictive_closure, math_synthesize_conditioned_closures, math_synthesize_gf2_vector_conditioned_access, math_discover_structural_conditioned_closure, math_discover_factor_swap_conditioned_closure
Projeções multimodais	math_projection_catalog, math_projection_create, math_projection_describe
Visualização	math_visualize, math_visualize_dag, math_render_koopman, math_visualize_projection, math_export_artifact
Sonificação	math_sonify, math_sonify_compare, math_sonification_describe, math_sonify_projection, math_export_audio
Artefatos multimodais	math_research_artifact_create, math_export_research_artifact
Conjuntos e lógica	math_set_create, math_set_op, math_set_membership, math_quantifier_check, math_quantifier_eliminate, math_quantifier_eliminate_batch
Polinômios	math_poly_groebner, math_poly_divide, math_poly_resultant, math_poly_discriminant, math_poly_factor, math_ideal_membership, math_poly_groebner_batch
Probabilidade	math_prob_rv_create, math_prob_expectation, math_prob_variance, math_prob_covariance, math_prob_bayes, math_prob_markov_stationary, math_prob_markov_hitting_time, math_prob_sample, math_prob_distribution
Estatística	math_stats_moments, math_stats_order, math_stats_regression, math_stats_correlation, math_stats_ttest, math_stats_chi2, math_stats_confidence_interval, math_stats_batch_moments
Tensores	math_tensor_create, math_tensor_get, math_tensor_contract, math_tensor_solve
Numéricos	math_root_find, math_root_scan, math_quadrature
EDO/EDP	math_ode_solve, math_ode_solve_numeric, math_ode_ensemble, math_pde_heat_1d, math_pde_heat_2d, math_pde_wave_1d, math_pde_advect_1d, math_pde_ensemble, math_pde_mol_heat
Otimização	math_optimize_critical_points, math_optimize_kkt, math_lp_solve, math_optimize_minimize, math_optimize_multistart
Unidades	math_unit_check, math_unit_convert, math_unit_simplify
Garantia	math_store_status, math_replay, math_fuzz_differential, math_certified_enclose
Prova	math_prove, math_prove_batch, math_prove_replay
Proveniência	math_derivation_get, math_derivation_trace

Cada docstring de ferramenta é escrita voltada para LLM: formatos de parâmetros, semânticas exatas-vs-numéricas, limites e dicas de acompanhamento são documentados no local.

Configuração

Todas as configurações são orientadas por ambiente com o prefixo MATHKERNEL_ (Settings.from_env()), inspecionáveis via math_capabilities:

Variável	Padrão	Propósito
MATHKERNEL_MAX_INPUT_LENGTH	100000	limite de entrada do parser
MATHKERNEL_MAX_OUTPUT_SIZE_BYTES	256000000	orçamento de bytes para resposta completa; cargas úteis superdimensionadas são preservadas como recursos verificados por integridade e retornadas por recibo
MATHKERNEL_SOLVER_TIMEOUT_SECONDS	30	orçamento de operações simbólicas usando trabalhadores de subprocesso limitados e canceláveis
MATHKERNEL_ENABLE_EXECUTION	false	execução de codegen em sandbox (opt-in)
MATHKERNEL_YOLO_MODE	false	desbloqueia math_yolo_settings para alterar configurações ativas de MATHKERNEL_* (coerção tipada; desligado por padrão)
MATHKERNEL_Z3_TIMEOUT_MS	10000	orçamento SMT (definido em cada instância do solver Z3)
MATHKERNEL_LEAN_BINARY / MATHKERNEL_LEAN_TIMEOUT_SECONDS	lean / 90	adaptador Lean (tempo limite passado para cada verificação lake env lean)
MATHKERNEL_SKIP_LEAN_INSTALL	não definido	pular o download padrão do Lean 4 + Mathlib
MATHKERNEL_LEAN_CACHE	cache da plataforma	raiz do espaço de trabalho elan + lake
MATHKERNEL_ENABLE_PARALLEL / MATHKERNEL_MAX_WORKERS	true / cpu_count	pools de processos e threads
MATHKERNEL_MAX_ITERATIONS	10000	limite de iterações para simplex / Nelder-Mead
MATHKERNEL_TOLERANCE	1e-12	tolerância numérica de convergência
MATHKERNEL_MAX_ODE_STEPS	100000	limite de passos de integração RK45
MATHKERNEL_STORE_PATH	não definido	persistência SQLite opt-in para expressões/derivações + math_replay
MATHKERNEL_PROVE_PORTFOLIO_SIZE	3	codificações SMT disputadas por chamada math_prove
MATHKERNEL_MAX_PDE_GRID	1000000	limite de células da grade do solver PDE
MATHKERNEL_MAX_PDE_FIELDS / MATHKERNEL_MAX_PDE_DIMENSIONS	16 / 8	limites tipados de campos PDE e variáveis independentes
MATHKERNEL_MAX_PDE_EQUATIONS / MATHKERNEL_MAX_PDE_TERMS	32 / 1024	limites tipados de sistema PDE e termos totais
MATHKERNEL_MAX_PDE_CONDITIONS	1024	limite total tipado de condições de contorno/iniciais
MATHKERNEL_MAX_PDE_DERIVATIVE_ORDER / MATHKERNEL_MAX_PDE_NONLINEAR_POWER	4 / 8	limites de derivadas e potências representadas
MATHKERNEL_MAX_PDE_WORK	2000000	limite de trabalho tipado de construção/replay PDE
MATHKERNEL_MAX_PDE_SPACES / MATHKERNEL_MAX_PDE_SPACE_ORDER	64 / 8	limites tipados de contagem de espaços de forma fraca e ordem de regularidade
MATHKERNEL_MAX_PDE_WEAK_TERMS / MATHKERNEL_MAX_PDE_IBP_STEPS	4096 / 256	limites tipados de termos integrais derivados e integração por partes
MATHKERNEL_MAX_PDE_WEAK_WORK	5000000	limite de trabalho de derivação/replay de forma fraca
MATHKERNEL_MAX_FEM_POINTS / MATHKERNEL_MAX_FEM_CELLS	100000 / 200000	limites de vértices/células da malha simplex
MATHKERNEL_MAX_FEM_DOFS	200000	limite de DOF do espaço de elementos finitos
MATHKERNEL_MAX_FEM_WORK	20000000	limite de trabalho de construção/replay de elementos finitos
MATHKERNEL_MAX_FEM_ASSEMBLY_NNZ / MATHKERNEL_MAX_FEM_ASSEMBLY_WORK	2000000 / 50000000	limites de entradas esparsas e trabalho de montagem
MATHKERNEL_MAX_FEM_EXACT_SOLVE_DOFS / MATHKERNEL_MAX_FEM_NUMERIC_SOLVE_DOFS	256 / 100000	limites de diagnóstico denso exato e solução esparsa numérica
MATHKERNEL_MAX_FEM_ESTIMATOR_WORK / MATHKERNEL_MAX_FEM_REFINED_CELLS	50000000 / 500000	limites de trabalho de replay do indicador residual e células de saída refinadas
MATHKERNEL_MAX_QE_VARIABLES	16	limite de variáveis para eliminação de quantificadores
MATHKERNEL_MAX_BATCH_JOBS	10000	limite de lote inteiro
MATHKERNEL_MAX_MATRIX_DIM	128	limite do mecanismo de matriz
MATHKERNEL_MAX_JOBS_RETAINED	100	retenção de trabalhos assíncronos
MATHKERNEL_MAX_MATH_OBJECTS	10000	limite de objetos tipados retidos
MATHKERNEL_MAX_CONTOUR_VERTICES	4096	limite de complexidade de contorno
MATHKERNEL_MAX_JOINT_DIMENSIONS	8	limite de dimensão de distribuição conjunta
MATHKERNEL_MAX_DISTRIBUTION_COMPONENTS	256	limite de componentes de mistura
MATHKERNEL_MAX_SYMBOLIC_SERIES_ORDER	128	limite de ordem de Laurent/classificação
MATHKERNEL_MAX_ORDER_STATISTIC_SAMPLE_SIZE	1024	limite de amostra simbólica de estatísticas de ordem
MATHKERNEL_MAX_GRAPH_VERTICES / MATHKERNEL_MAX_GRAPH_EDGES	4096 / 65536	limites tipados de tamanho de grafo
MATHKERNEL_MAX_COMBINATORIAL_ITEMS	10000	limite de geração combinatória preguiçosa
MATHKERNEL_MAX_GROUP_ELEMENTS	4096	limite de enumeração de grupos finitos
MATHKERNEL_MAX_FIELD_DEGREE	64	limite de grau de extensão GF(p^m)
MATHKERNEL_MAX_NORMAL_FORM_DIM	128	limite de dimensão de matriz Smith/Hermite
MATHKERNEL_MAX_INVERSE_BRANCHES	256	limite de ramo/Jacobiano de mudança de variável
MATHKERNEL_MAX_OBLIGATION_STEPS	128	obrigações máximas de plano executável
MATHKERNEL_MAX_FWHT_SIZE	2²⁰	limite de comprimento FWHT
MATHKERNEL_MAX_FINITE_STATES	4096	limite de enumeração de sistemas finitos
MATHKERNEL_MAX_CUMULANT_ORDER	8	limite de ordem de cumulantes/tensores conectados
MATHKERNEL_MAX_CLOSURE_RESULTS	10000	limite de resultados de busca de fechamento
MATHKERNEL_MAX_GEOMETRY_DIMENSION	8	limite de dimensão de variedade/gráfico
MATHKERNEL_MAX_GEOMETRY_RANK	6	limite de posto de campo tensorial denso
MATHKERNEL_MAX_GEOMETRY_POINTS	10000	limite de contagem de pontos/vértices
MATHKERNEL_MAX_GEOMETRY_SIMPLICES	100000	limite de contagem de semiespaços/triângulos
MATHKERNEL_MAX_GEOMETRY_WORK	1000000	limite de trabalho simbólico de geometria de pré-verificação
MATHKERNEL_MAX_TOPOLOGY_DIMENSION	16	grau máximo de complexo finito/dimensão ambiente
MATHKERNEL_MAX_TOPOLOGY_CELLS	10000	limite total de células de base simplicial/cúbica/cadeia
MATHKERNEL_MAX_TOPOLOGY_MATRIX_ENTRIES	1000000	limite de entradas armazenadas de matriz de fronteira
MATHKERNEL_MAX_TOPOLOGY_ENTRY_BITS	4096	limite de comprimento de bits de entradas de fronteira inteiras
MATHKERNEL_MAX_TOPOLOGY_WORK	2000000	limite de trabalho de pré-verificação de topologia exata
MATHKERNEL_MAX_STATISTICAL_VARIABLES	256	limite tipado de colunas de amostra
MATHKERNEL_MAX_STATISTICAL_OBSERVATIONS	100000	limite tipado de linhas de amostra
MATHKERNEL_MAX_STATISTICAL_CELLS	1000000	limite tipado de células retangulares de amostra
MATHKERNEL_MAX_STATISTICAL_WORK	2000000	limite de trabalho de pré-verificação descritiva/covariância
MATHKERNEL_MAX_GLM_PARAMETERS	64	limite de coeficientes ajustados, incluindo o intercepto
MATHKERNEL_MAX_GLM_ITERATIONS	200	limite de iterações IRLS solicitadas
MATHKERNEL_MAX_GLM_PREDICTION_ROWS	100000	linhas de média condicional por solicitação de previsão
MATHKERNEL_MAX_GLM_WORK	20000000	limite de trabalho de pré-verificação de posto/matriz/iteração GLM
MATHKERNEL_MAX_NONPARAMETRIC_GROUPS	64	limite de grupos Kruskal–Wallis selecionados
MATHKERNEL_MAX_EXACT_RESAMPLING_STATES	100000	limite de estado completo de sinais/rótulos/permutações
MATHKERNEL_MAX_RESAMPLES	1000000	limite de sorteios de permutação/bootstrap Monte Carlo
MATHKERNEL_MAX_RESAMPLING_BATCH_CELLS	1000000	células geradas por lote de bootstrap
MATHKERNEL_MAX_RESAMPLING_WORK	20000000	limite de trabalho de pré-verificação de posto/enumeração/reamostragem
MATHKERNEL_MAX_SURVIVAL_STRATA	64	limite de estratos de sobrevivência distintos
MATHKERNEL_MAX_SURVIVAL_TIMELINE_POINTS	100000	limite de linha do tempo Kaplan–Meier selecionada
MATHKERNEL_MAX_COX_PARAMETERS	64	limite de preditores Cox
MATHKERNEL_MAX_COX_ITERATIONS	200	limite de iterações Newton Cox solicitadas
MATHKERNEL_MAX_COX_PREDICTION_ROWS	100000	limite de linhas de previsão de risco parcial
MATHKERNEL_MAX_COX_INFORMATION_CONDITION	1000000000000	teto de condição de informação observada
MATHKERNEL_MAX_SURVIVAL_WORK	20000000	limite de trabalho de conjunto de risco/matriz/iteração de sobrevivência
MATHKERNEL_MAX_TIME_SERIES_LAG	1000	limite de defasagem ACF/PACF/diagnóstico
MATHKERNEL_MAX_TIME_SERIES_DIFFERENCE	2	limite de ordem de diferenciação ARIMA
MATHKERNEL_MAX_TIME_SERIES_PARAMETERS	32	limite de parâmetros dinâmicos AR/MA/GARCH
MATHKERNEL_MAX_TIME_SERIES_ITERATIONS	500	limite de iterações do otimizador de ajuste
MATHKERNEL_MAX_TIME_SERIES_FORECAST_STEPS	10000	limite de horizonte de previsão
MATHKERNEL_MAX_TIME_SERIES_WORK	50000000	limite de trabalho de análise/ajuste/previsão
MATHKERNEL_MAX_STOCHASTIC_STATES	256	limite de estado CTMC
MATHKERNEL_MAX_STOCHASTIC_TIME_POINTS	10000	limite de tempo de previsão/dimensão finita
MATHKERNEL_MAX_GP_CONDITIONING_POINTS	2000	limite de observações GP
MATHKERNEL_MAX_STOCHASTIC_MATRIX_ENTRIES	1000000	limite de espaço de trabalho de covariância/gerador
MATHKERNEL_MAX_GP_CONDITION_NUMBER	1000000000000	teto de condicionamento GP
MATHKERNEL_MAX_STOCHASTIC_WORK	50000000	limite de trabalho de fatoração/exponencial
MATHKERNEL_MAX_SDE_STATE_DIMENSION	32	limite de dimensão de estado SDE
MATHKERNEL_MAX_SDE_NOISE_DIMENSION	32	limite de dimensão do driver Browniano
MATHKERNEL_MAX_SDE_STEPS	1000000	limite de passos de simulação/convergência
MATHKERNEL_MAX_SDE_PATHS	100000	limite de caminhos de simulação
MATHKERNEL_MAX_SDE_SIMULATION_CELLS	5000000	limite de células de caminho/incremento aleatório armazenado
MATHKERNEL_MAX_SDE_WORK	50000000	limite de trabalho de atualização SDE
MATHKERNEL_MAX_SDE_QUERY_VALUES	20000	valores de caminho/terminal retornados por consulta

Layout do repositório

src/mathkernel/            core library, typed mathematics and kernel facade
src/mathkernel_mcp/        FastMCP server layer and public math_* tools
src/mathkernel_projection/ shared typed multimodal projection layer
src/mathkernel_viz/        visualization IR, viewers and portable renderers
src/mathkernel_sonify/     scientific sonification IR, PCM/WAV and WebAudio
src/mathkernel_artifacts/  shared evidence, lineage and synchronization schema
src/mathkernel_multimodal/ unified visual/audio research-artifact exporter
ui/studio/                optional local Studio authoring/inspection preview
scripts/                   reproducibility, GPU checks and demonstrations
experiments/               research validation programs and datasets
skills/                    synchronized Python and MCP agent skills
tests/                     core, regression, multimodal and domain test suites
benchmarks/                correctness-gated performance measurements

Pacotes de habilidades

O MathKernel inclui dois pacotes de habilidades de agente sincronizados: um para uso direto em Python e um para clientes MCP. Eles documentam o mesmo contrato de evidência, ciclo de vida de objetos e semântica matemática, adaptando exemplos às suas respectivas interfaces.

As habilidades cobrem trabalho simbólico/exato, raciocínio e prova, persistência, dinâmica finita, probabilidade/estatística, numérica, tensores/unidades, desempenho, visualização, sonificação científica e o fluxo de trabalho compartilhado de projeção multimodal. As habilidades de viz/áudio agora exigem proveniência de projeção em primeiro lugar para objetos estruturados e redução explícita de alta dimensão ou extração acústica em vez de achatamento oculto.

Testes

Execute a suíte completa da árvore de fontes com as dependências opcionais exigidas pelos domínios que você deseja validar:

PYTHONPATH=src:. python -m pytest -q
python scripts/gpu_smoke.py

O repositório degrada mecanismos opcionais indisponíveis para unknown ou unavailable em vez de fabricar sucesso. FastMCP é necessário para testes de registro MCP, z3-solver para testes de SMT/prova/eliminação de quantificadores, e o runtime ANTLR compatível para análise LaTeX do SymPy. Módulos de teste específicos de domínio e executores de experimentos podem ser executados independentemente ao validar uma superfície matemática específica.

A cobertura inclui análise e tratamento de ambiguidade, álgebra simbólica e cálculo, aritmética exata de inteiros e campos finitos, algoritmos de grafos, álgebra linear, caminhos diferenciais Numba/CUDA, trabalhos assíncronos, geração e verificação de código, métodos GF(2) e Fourier finito, dinâmica Koopman/finita, análise PRNG, matemática de engenharia tipada, geometria/topologia, estatística e sistemas estocásticos, PDE/FEM/adaptividade, propagação de evidências, integridade de persistência, visualização, sonificação, artefatos multimodais e a superfície de ferramentas MCP.

CI tem como alvo versões suportadas de Python com fan-out nativo de threads limitado por trabalhador. As verificações de distribuição constroem o sdist e a wheel, verificam metadados, instalam a wheel em um ambiente limpo, confirmam a versão do runtime e verificam que os ativos offline de visualização/multimodal fornecidos estão presentes. Exportações portáteis, portanto, não exigem CDN após a instalação.

Limites de segurança

• Nenhuma expressão bruta do usuário chega a sympify()/parse_expr(); gramática restrita, funções desconhecidas rejeitadas, notação ambígua recusada com candidatos.
• Conversão de inteiros de comprimento arbitrário em partes; guardas de saída de resultados grandes; trabalho automático de teoria dos números limitado; tetos de passos de obrigação; validação de dependência/ciclo.
• Execução de código em sandbox é opt-in (MATHKERNEL_ENABLE_EXECUTION=1), roda em um subprocesso isolado com tempo limite e é sempre rotulada como evidência numérica.
• Invocação de subprocesso Lean usa shell=False; mecanismos opcionais relatam unknown/unavailable em vez de fabricar sucesso.
• Buscas externas nativas de candidatos LP/QP/MILP, cônicos/QCQP, Riccati/LQG e posicionamento de polos numéricos rodam em interpretadores novos cujos grupos de processos são mortos no tempo limite. Solicitações/resultados são limitados e o fan-out BLAS/OpenMP é limitado.
• Persistência SQLite verifica cada payload JSON com SHA-256 antes de decodificar. registros tipados canônicos adicionalmente reconciliam seu tipo de objeto declarado, classe de modelo decodificada e campo de link de origem antes da recuperação ou execução. Registros corrompidos ou substituídos falham de forma fechada sem produzir objetos derivados.

Este limite de terminação não é uma sandbox de código hostil e não impõe uma cota de memória do SO. Isolamento multi-tenant ainda pertence a um trabalhador externo ou camada de sandbox.

Licença

Copyright © 2026 Maarten Boone.

Lançado sob a Licença MIT.