MathKernel：让LLM数学计算有据可查
MathKernel: An evidence-aware multi-engine mathematics kernel and MCP server
大语言模型擅长理解数学意图，却在算术计算上频频出错。MathKernel 作为一个证据感知的多引擎数学内核，旨在扭转这一局面。它将 LLM 的角色限定为解析意图与规划，而将精确计算、符号推导及形式化验证交给内核处理。无论是作为 Python 库还是 MCP 服务器，MathKernel 都能为每一次计算结果打上明确的信任标签，并记录完整的推导路径。从精确算术到形式化证明，它确保近似输入的祖先信息不会无声消失，让数学结果不再是黑盒，而是拥有可追溯证据的可靠结论。
LLM 负责解读意图，而 MathKernel 则负责确立数学证据。
- nxobject
顺便提一下，"MathKernel"这个名字有重名问题——Mathematica 自己的内核可执行文件就叫这个名字，当你现有的工具已经引用它时，这有点不太方便。
- overfitCNN
我正在这个领域开发一个名为 Alkahest 的项目：https://github.com/alkahest-cas/alkahest。这是一个用 Rust 编写的计算机代数系统，能为其许多操作生成对应的 Lean 证书，从而实现形式化验证。
Alkahest 可作为 Python 库或 Rust crate 使用。它专为智能体（agent）设计，提供出色的调试输出。
我正在快速迭代该项目，欢迎随时向我发送任何问题、评论或想法。
- xvilka
你也可以为大多数符号数学添加对 Woxi[1][2] 的支持，而且它应该比在不同 Python 库之间打补丁要快得多。