MathCode 0.2.0 发布：前缀缓存技术使大模型 API 成本骤降九成
Math-AI 团队于 2026 年 5 月 27 日正式发布数学形式化与定理证明 AI 智能体 MathCode 0.2.0。该版本通过创新的前缀缓存（Prefix Caching）请求整形与策略控制机制，实现 API 成本降低高达 90%，为长程证明和多轮交互场景下的高额开销问题提供了突破性解决方案。
前缀缓存：解决 LLM 推理成本痛点
在大语言模型应用中，高达 70% 的提示词存在重复或相似内容。传统缓存方式依赖全文匹配，仅能处理完全相同或高度相似的查询。而前缀缓存技术则将请求中的共同前缀（即 KV 缓存状态）存储并复用，使包含相同前缀但后续内容不同的请求也能享受缓存加速。
MathCode 0.2.0 针对定理证明场景的特殊需求——模型需频繁读取庞大代码库与公理库——引入了 Prefix-cache request-shape diagnostics and policy controls 机制。系统通过屏蔽提示词头部归属以保障结构稳定性，新增多项缓存优化功能：
- 多断点缓存（
MATHCODE_CACHE_MULTI_BREAKPOINT）：支持在多个位置设置缓存断点 - 显式最小前缀网关：精确定义缓存生效的前缀范围
- 空闲感知 TTL 策略：智能调整缓存生命周期
这些优化通过底层请求形状对齐最大化 Provider 原生缓存命中率，将长会话账单压至原本的一成。
任务管理与思考深度控制
为防止长程运行导致成本超支，新版本引入 Token 预算上限控制功能。开发者可通过 MATHCODE_GOAL_MAX_TOKEN_BUDGET 设定预算上限，同时限制嵌套斜杠命令数量以防范无限循环风险。
证明会话还支持通过 --effort 或 /effort 参数动态调整思考深度，提供 low、medium、high、max 四个级别，并可随时退回默认配置，满足不同复杂度的证明需求。
编译加速与部署简化
MathCode 0.2.0 新增对 Project Numina 开发的 Kimina Lean Server 编译器的支持，可作为子进程常驻运行，编译检查请求路由至 /verify 接口。此外，安装脚本 setup.sh 迎来重构，新增 --status、--clean 等指令，支持 release 校验和自动验证，并复用系统 Lean/Lake 环境，显著降低部署门槛。