形式化证明与代码生成的结合正在打开可信编程的新篇章。Mistral 近日开源的 Leanstral 定位为首个面向 Lean 4 的编程代理，以仅 6B 活跃参数的稀疏架构，在 FLTEval 基准上实现了令人瞩目的性价比：pass@2 得分 26.3，成本仅需 36 美元，而 Claude Sonnet 4.6 达到相近得分需 549 美元。这一数字背后折射出形式化证明工程化的核心命题 —— 如何在保证证明正确性的前提下显著降低推理成本。
Leanstral 的设计目标并非单纯追求数学竞赛成绩，而是聚焦于「真实形式化仓库中的证明工程任务」。这一定位使其区别于此前聚焦于孤立数学题目的证明助手。团队构建了 FLTEval 评估套件，模拟完整 PR 场景：模型需要完成所有形式化证明并正确定义新的数学概念，而非解答单一定理。这种评估方式更贴近实际开发流程，也更能反映模型在生产环境中的可用性。
从架构角度看，Leanstral 采用高度稀疏化设计，显著降低了推理时的算力消耗。配合 Lean 4 作为完美验证器进行并行推理，模型能够在证明失败时快速获得反馈并调整策略。Mistral 还强调该模型针对 MCP（Model Context Protocol）进行了专门优化，尤其是与 lean-lsp-mcp 的协作，这使得将其集成到现有开发工作流中的门槛大幅降低。
在实际应用层面，团队展示了两个典型场景。其一是解答 Proof Assistants Stack Exchange 上的真实问题：用户报告某脚本在 Lean 4.29.0-rc6 版本中无法编译。Leanstral 不仅成功复现了问题环境，还定位到根本原因 ——def 关键字创建的刚性定义阻塞了 rw 策略的模式匹配，并给出了将 def 替换为 abbrev 的解决方案。其二是将 Coq 代码迁移至 Lean：模型从普林斯顿大学的形式化语言课程材料出发，成功完成了概念转换并实现了自定义记号，甚至能在此基础上证明程序属性。
当前 Leanstral 已通过三条渠道开放使用：集成在 Mistral Vibe 中可直接通过 /leanstall 命令启动；提供免费或低价的 API 端点 labs-leanstral-2603；以及在 Apache 2.0 许可证下开放模型权重下载。对于希望在代码生成流程中引入形式化验证的团队而言，Leanstral 提供了一个低门槛的切入点 —— 既无需依赖昂贵的闭源模型，也无需从零构建证明基础设施。
资料来源：Mistral AI 官方发布页面（https://mistral.ai/news/leanstral）