通过 MCP 为智能体提供多引擎数学核心函数

MathKernel是一款注重证据的多引擎数学核心库，以MCP服务器形式提供，供智能体使用。

具体怎么做

MathKernel 作为 MCP 服务器运行（版本：mathkernel-mcp，stdio，包含 162 种数学工具）。模型负责解析与规划，而内核则通过 SymPy、Z3、Lean、mpmath 以及 numba/CUDA 进行计算。典型会话流程包括：识别功能、解析表达式、创建上下文，然后调用 math_reason 进行求解与验证。长周期任务则通过异步作业处理。每个结果都带有信任标签和推导路径。

做到了什么

原文未提供任何基准值或结果数据。它仅记录了设计方案：信任度以最薄弱的证据为上限，而小数输入则将其结果转换为数字形式，从而阻碍了 Lean 和 SMT 验证。

上手要点

除非设置 MATHKERNEL_SKIP_LEAN_INSTALL=1，否则在首次服务器启动时需安装 Lean 4 和 Mathlib。CUDA 需要额外的 nvidia pip 包，否则将退化为使用 CPU。