事实证明，人工智能代理是代码生成方面功能强大的工具。然而，当我们将这些模型推向从前沿研究数学到关键任务软件的高风险领域时，我们遇到了一个扩展瓶颈：人工审查。手动验证所需的时间和专业知识成为工程速度的主要障碍。

我们设想一代更有帮助的编码代理，以执行他们的任务并根据严格的规范正式证明他们的实现。人类不是调试机器生成的逻辑，而是决定他们想要什么。今天，我们正在朝着这一愿景迈出重要的第一步。

介绍 Leanstral

我们发布了 Leanstral，这是第一个专为 Lean 4 设计的开源代码代理。Lean4 是一个证明助手，能够表达复杂的数学对象，例如完美状空间和软件规格，如Rust 碎片的特性。与充当大型通才模型包装器或专注于单一数学问题的现有证明系统不同，Leanstral 的设计非常高效（具有 6B 个活动参数），并经过训练可在实际的正式存储库中运行。

• 开放且可访问：我们在 Apache 2.0 许可证下、在 Mistral 氛围内以代理模式并通过免费 API 端点发布 Leanstral 权重。我们还将发布一份技术报告，详细介绍我们的训练方法，以及新的评估套件 FLTEval，以使评估不再只关注竞赛数学。

• 高效而强大：我们为 Leanstral 使用高度稀疏的架构，并针对证明工程任务对其进行了优化。Leanstral 利用 Lean 的并行推理作为完美的验证器，与现有的闭源竞争对手相比，它的性能和成本效益都很高。

• 可通过 MCP 升级：Leanstral 通过 vivi 支持任意 MCP，并经过专门培训，可通过常用的lean-lsp-mcp 实现最大性能。 

评价

为了反映在实际证明工程场景中的实用性，我们对 Leanstral 进行了基准测试，以完成所有形式证明并在 FLT 项目的每个 PR 中正确定义新的数学概念，而不是孤立的数学问题。我们将 Leanstral 与领先的编码代理（Claude Opus 4.6、Sonnet 4.6、Haiku 4.5）和开源模型（Qwen3.5 397B-A17B、Kimi-K2.5 1T-A32B、GLM5 744B-A40B）进行比较。

Leanstral 与 OSS 模型

Leanstral-120B-A6B 与规模大得多的开源同行相比，具有显着的效率优势。虽然像 GLM5-744B-A40B 和 Kimi-K2.5-1T-32B 这样的模型很难扩展，它们的 FLTEval 分数分别约为 16.6 和 20.1，但 Leanstral 只需一次传递就超越了它们。

即使是 Qwen3.5-397B-A17B（所示的最强 OSS 竞争对手）也需要 4 次通过才能达到 25.4 的分数。相比之下，Leanstral 以一半的投资 (pass@2) 获得了 26.3 的优异分数，并继续线性扩展，在相同成本水平下达到 29.3。

Leanstral vs. 克劳德家族

Leanstral 是 Claude 套件的高价值替代品，以低廉的价格提供具有竞争力的性能：Leanstral pass@2 的得分为 26.3，比 Sonnet 高出 2.6 分，而运行成本仅为 36 美元，而 Sonnet 的运行成本为 549 美元。在 pass@16 时，Leanstral 的得分为 31.9，轻松击败 Sonnet 8 分。虽然 Claude Opus 4.6 在质量方面仍然处于领先地位，但其成本却高达 1,650 美元，比运行 Leanstral 高出 92 倍。

在我们的基准测试中，我们使用 Mistral Vibe 作为支架，没有专门针对评估进行修改。

案例研究

回答有关最新精益版本变化的 stackexchange 帖子

当新的精益版本发生重大更改时，迁移代码可能会非常令人头疼。我们喂Leanstral来自 Proof Assistants Stack Exchange 的现实问题关于一个在 Lean 4.29.0-rc6 中神秘地停止编译的脚本（由于其新近，我们没有使用它进行训练）。罪魁祸首是重写（读写）策略突然无法匹配涉及简单类型别名的模式，最初写为def T2 := 布尔列表。

Leanstral 没有在黑暗中冒险，而是卷起了袖子。它成功构建了测试代码来重新创建失败的环境，并通过定义等式诊断出根本问题。该模型正确地识别出，因为 def 创建了一个需要显式展开的严格定义，所以它主动阻止 rw 策略看到它需要匹配的底层结构。

它提出的解决方案很简单：只需交换定义为了缩写。因为缩写创建一个透明别名，它在定义上立即等于原始类型，读写战术可以再次完美匹配模式(L2 n).长度在证明中。Leanstral 完成了这项工作，并向用户完美地解释了原理。 

关于程序的推理

我们复制了 Rocq 中的定义https://www.cs.princeton.edu/courses/archive/fall10/cos441/sf/Imp.html并要求 Leanstral 转变为精益。它成功地做到了这一点，甚至实现了自定义符号。示例片段：

它还可以翻译为 Lean，然后在给出 Rocq 语句时证明该语言程序的一些属性（无需证明）：

需求证明。立即尝试 Leanstral。

Leanstral 现已可供所有人使用。

• 零设置米斯特拉尔氛围：我们已将 Leanstral 直接集成到 Mistral Vibe 中，以进行即时、零设置的 Vibe 编码和验证。使用/leanstall开始。

• 实验室 API：通过我们的免费/接近免费的 API 端点访问模型实验室-leanstra-2603。我们将在有限的时间内保持此端点的高度可访问性，以收集真实的反馈和可观察性数据，为下一代经过验证的代码模型提供动力。

• 拥有权重：下载 Apache 2.0 许可模型并在您自己的金属上运行它。

文档-注册米斯特拉尔氛围