为什么数学能力突然成了 Agent 工程的硬需求 2026 年下半年,关于"LLM 能不能做高等数学"的争论正在被工程化地回答。过去两年,业界逐渐达成一个不太舒服的共识:LLM 能"答"数学题,但这种答题靠的是训练语料里见过的解法,而不是真正在脑子里推导。一旦遇到需要严格证明或者多步精确推导的场景,LLM 输出的答案无法保证数学意义上的正确。这意味着在金融建模、密码学验证、控制工程、科学研究等任何
为什么数学能力突然成了 Agent 工程的硬需求
2026 年下半年,关于"LLM 能不能做高等数学"的争论正在被工程化地回答。过去两年,业界逐渐达成一个不太舒服的共识:LLM 能"答"数学题,但这种答题靠的是训练语料里见过的解法,而不是真正在脑子里推导。一旦遇到需要严格证明或者多步精确推导的场景,LLM 输出的答案无法保证数学意义上的正确。这意味着在金融建模、密码学验证、控制工程、科学研究等任何对正确性有严格要求的场景里,把数学任务直接交给 LLM 都是有问题的。
在这种背景下,2026 年 9 月一个叫 MathKernel 的开源项目在 GitHub 上线,迅速进入了 Hacker News 的显眼位置。它给自己的核心定位写得很直接:LLM 解释意图,MathKernel 建立数学证据。它提供的不是又一个大模型,而是一个 evidence-aware 的多引擎数学 kernel,可以作为 Python 库调用,也可以作为 MCP server 被任何支持 MCP 协议的 Agent 调用。这个定位决定了一件关键的事:它不试图让 LLM 自己做数学,而是把数学这件事从 LLM 的推理里分离出来,作为单独的可验证模块运行。
MathKernel 的核心机制:trust level 与 derivation trail
MathKernel 在架构上和一般数学库最大的区别,在于它给每一条数学结果都打上显式的信任级别、引擎标签和推导路径。这三个属性合在一起回答了一个非常基础的问题:这条结论到底是怎么来的、能被信到什么程度。在 MathKernel 的设计里,精确计算、已检查的证书、符号结果、有认证的闭包、经验证据和形式化证明是六种不同的数学声明,它们在信任级别上是严格区分的。
这种区分非常关键。一个工程师最常见的误判就是把"算得对"等同于"证明了对"。精确算术本身就是形式化证明吗?不是。把一个浮点数结果当成形式化结论是危险的。同样,如果一个计算依赖近似输入,这条近似关系必须保留在结果里,不能悄悄消失。这就是 MathKernel 引入 derivation trail(推导路径)的原因。每一条结果都附带它是怎么来的信息,包括用了哪个引擎、做了什么近似、引用了什么公理或者前序结论。
MathKernel 的引擎组合也反映了它的工程态度:它把 sympy、z3、lean、numba、cuda 这些不同范式的数学工具组合在一起。sympy 做符号计算,z3 做 SMT 求解,lean 做形式化证明,numba 做数值加速。这种组合不是说这些工具擅长的事都一样,而是说每个工具擅长的事不一样 —— 一个真实的数学问题往往需要不同引擎接力才能解决,MathKernel 的 orchestration 层负责调度这种接力。
从 evidence-aware 到 MCP:让 Agent 能消费数学能力
MathKernel 同时提供 Python 库和 MCP server 两种形态,这个选择是工程化的。MCP 是当下主流 Agent 框架的事实标准接口,几乎所有 Harness 都支持。MathKernel 把数学能力封装成 MCP server,意味着任何 Coding Agent —— Claude Code、Codex CLI、Copilot CLI、Qwen Code 这些 —— 只要把 MathKernel server 注册到自己的 MCP 配置里,就能在自己的工具菜单里多出一个"做数学"的工具,而不需要修改 Agent 框架的内核代码。
这种"通过 MCP server 而不是私有协议接入"的做法,和 SagaShield 把事务语义做成运行时,以及 Stroq 把工具输出拦截做成 session 层,在思路上是同构的:把过去需要修改框架内核才能解决的能力,做成可以独立部署的模块。这种模块化思路让 Agent 的能力扩展成本从"修改框架"降到了"启动一个 server"。
在 trust model 的设计上,MathKernel 把六种数学声明做了严格的层级划分。形式化证明是最高的,它来自 Lean 这样的定理证明器,每一行推导都有机器可检查的证据。精确计算次之,它来自 SymPy 这种符号引擎,结果是数学上的精确表达,但本身不构成证明。认证闭包来自 SMT 求解器或区间算术,能给出一个真实解所在的范围,适合需要"虽然我不知道确切值但我知道它在哪儿"的场景。经验证据来自蒙特卡洛或者近似数值方法,适合"在合理的精度下答案是这样"的场景。最弱的是启发式结果,完全依赖 LLM 自己的推理,MathKernel 不推荐把这种结果当成数学结论来用。
另一个独立视角:Alkahest 和形式化证明
几乎在 MathKernel 上线的同时,HN 评论里有人提到一个独立项目 Alkahest:一个用 Rust 写的计算机代数系统,能给很多操作产出对应的 Lean 证书,这些证书可以被形式化验证。Alkahest 同时提供 Python 库和 Rust crate,设计上也考虑了 Agent 使用,输出对调试友好。这个项目和 MathKernel 在工程取舍上有一个明显差异:MathKernel 把 sympy/z3/lean 当作不同引擎组合,Alkahest 则把 Lean 当作证明质。
这个差异背后是两种不同的工程哲学。MathKernel 的多引擎策略承认一个现实:不是所有数学问题都能被形式化证明,大多数问题需要"够用就好"的工程答案,精确计算、闭包、近似数值都各有各的场景。Alkahest 的形式化证明策略承认另一个现实:在科研和密码学场景里,"够用就好"是不够的,必须有机器可检查的证明。两套路径都成立,服务于不同的数学问题。
对工程落地的启示是:科研 Agent 在做数学时,应当根据任务的"硬要求"选择工具。数值模拟、近似计算、符号推导这类任务用 MathKernel 风格的多引擎就够,代码验证、定理证明、形式规约这类任务用 Alkahest 风格的形式化证明更稳。一个真正严肃的科研 Agent,通常需要把这两类工具都接进自己的工具链,而不是二选一。
科研 Agent 的工程拐点
MathKernel 这一类工具的出现,代表了 Agent 工程的一个关键拐点:从"让模型自己解决一切"转向"让模型调用专业模块"。LLM 解释意图、判断何时调用、调参、整合结论,而专业模块负责真正的"做事"。这种分工的合理性在于,LLM 在判断何时该用哪个模块上有跨领域的通用性,但在每个具体模块的深度上不如专门的工具。
在科研 Agent 这个具体场景里,这种分工带来的影响有三层。第一层是结果可信度提升:LLM 直答数学题的可信度依赖运气,Agent 调用 MathKernel 然后信任模块结果的可信度依赖模块本身的能力 —— 后者是有工程边界的、可审计的。第二层是工作流可解释:LLM 直答时,中间步骤不透明;Agent 调用工具时,每一步的工具调用、参数、结果都有完整记录,事后复盘可以重新跑同样的问题。第三层是失败可恢复:LLM 直答错了一个数字,可能整篇论文的结论就被污染;Agent 调用工具时,如果某个工具算错了,可以单独换工具重新算,而不需要重新生成整篇论文。
这个分工对科研 Agent 的工程基线有三条具体启示。第一条是科研 Agent 必须把数学能力作为外部工具,而不是依赖 LLM 自己推导。第二条是 Agent 调用数学工具时,必须保留工具调用的完整日志,包括用了哪个引擎、传了什么参数、得了什么结果。第三条是科研 Agent 必须支持"工具结果质疑"机制 —— 如果某个工具返回的结果和其他工具、或者和已有数据不一致,Agent 应当自动标记并触发复核,而不是默默接受。
企业落地的基线考量
把 MathKernel、Alkahest 这类工具的出现综合起来看,可以为企业开发一个科研 Agent 划出四条基线。第一条基线是科研 Agent 必须有可调用的形式化数学模块,而不是单纯依赖 LLM 自己推导。这条基线决定了 Agent 输出的可信度上限,任何单纯依赖 LLM 直答的 Agent 都应该被视为不可信。
第二条基线是数学工具的输出必须附带 trust level 和 derivation trail。这条基线保证了 Agent 的输出在企业合规审计时有可追溯的证据链。一个数学结论如果是"精确计算",就要标"精确计算";如果是"形式化证明",就要标"形式化证明"。这两种结论在科研论文里的引用方式是不同的。
第三条基线是科研 Agent 必须有质疑自身结论的机制。一个数字算出来之后,Agent 应该有能力用另一个独立的引擎验证一遍,如果两个引擎的结果不一致,就要标出"待复核"。这种"被动式"验证,本质上是把科研论文的同行评审机制做进了 Agent。
第四条基线是数学工具的版本和引擎组合必须可记录、可复现。一篇科研论文如果依赖某个 Agent 的某个数学结论,后续任何人复现这篇论文时都应该能拿到完全相同的数学结果。这要求 MathKernel 这类工具在每次计算时记录完整的版本栈和参数,而不是像 LLM 直答那样只给一个最终数字。
把以上四条放在一起,可以画出 2026 年下半年科研 Agent 落地的工程基线:数学能力外置,数学结论可追溯,数学结果可质疑,数学过程可复现。这四条不是某一个工具能做到的,而是整个 Agent 工具生态的成熟度。MathKernel、Alkahest 这一类工具的出现,说明这套基线在工具层面已经开始具备落地的可能性。科研 Agent 从"能聊天"到"能写论文"的转变,正在这四条基线上一条一条地落地。
