AI 智能体已被证明是代码生成方面能力极强的工具。然而，当我们将这些模型推向高风险领域——从前沿研究数学到任务关键型软件——时，我们遇到了一个规模化瓶颈：人工审查。手动验证所需的时间和专业知识成为工程速度的主要阻碍。
我们设想一代更有帮助的编码智能体，既能执行任务，又能针对严格规范形式化证明其实现。人类不再调试机器生成的逻辑，而是规定他们想要什么。今天，我们朝着这一愿景迈出了重要的第一步。
推出 Leanstral
我们发布 Leanstral，这是首个专为 Lean 4 设计的开源代码智能体。Lean4 是一个证明助手，能够表达复杂的数学对象，例如完美胚空间，以及软件规范，例如 Rust 片段的性质。与现有那些充当大型通用模型包装器或专注于单一数学问题的证明系统不同，Leanstral 被设计为高度高效（拥有 6B 活跃参数），并针对在现实形式化代码库中运行进行了训练。
开放且易获取：我们以 Apache 2.0 许可证发布 Leanstral 权重，在 Mistral vibe 中以智能体模式提供，并通过免费 API 端点提供。我们还将发布一份详细说明我们训练方法的技术报告，以及一套新的评估套件 FLTEval，以使评估不再局限于竞赛数学。
高效且强大：我们为 Leanstral 使用了高度稀疏的架构，并针对证明工程任务对其进行了优化。利用以 Lean 作为完美验证器的并行推理，Leanstral 相对于现有的闭源竞争对手既性能出色又具有成本效益。
可通过 MCP 升级：Leanstral 通过 vibe 支持任意 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 与开源模型对比
Leanstral-120B-A6B 相较于其规模大得多的开源同行展现出显著的效率优势。虽然 GLM5-744B-A40B 和 Kimi-K2.5-1T-32B 等模型难以扩展，其 FLTEval 分数分别止步于约 16.6 和 20.1，但 Leanstral 仅用单次尝试就超越了这两者。
即便是所示最强的开源竞争对手 Qwen3.5-397B-A17B，也需要 4 次尝试才能达到 25.4 分。相比之下，Leanstral 以一半的投入（pass@2）取得了更优的 26.3 分，并继续线性扩展，在相同成本水平下达到 29.3 分。
Leanstral 与 Claude 系列对比
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 作为脚手架，未针对评估做任何修改。
| 模型 | 成本（美元） | 得分 |
|---|---|---|
| Haiku | 184 | 23.0 |
| Sonnet | 549 | 23.7 |
| Opus | 1,650 | 39.6 |
| Leanstral | 18 | 21.9 |
| Leanstral pass@2 | 36 | 26.3 |
| Leanstral pass@4 | 72 | 29.3 |
| Leanstral pass@8 | 145 | 31.0 |
| Leanstral pass@16 | 290 | 31.9 |
案例研究
回答关于最新 Lean 版本变更的 stackexchange 帖子
当破坏性变更出现在新的 Lean 版本中时，迁移代码可能会非常令人头疼。我们向 Leanstral 提供了来自 Proof Assistants Stack Exchange 的一个真实问题，内容是关于一个在 Lean 4.29.0-rc6（由于其较新，我们未用其进行训练）中神秘地停止编译的脚本。罪魁祸首是一个重写（rw
）策略，它突然无法匹配涉及简单类型别名的模式，该别名最初写为 def T2 := List Bool
。
Leanstral 没有盲目猜测，而是卷起袖子动手解决。它成功构建了测试代码来重现失败的环境，并诊断出定义相等性方面的根本问题。该模型正确地识别出，由于 def 创建了一个需要显式展开的刚性定义，它主动阻止了 rw 策略看到其需要匹配的底层结构。
它提出的修复很简单：只需将 def
换成 abbrev
。因为 abbrev
创建了一个透明的别名，该别名立即与原始类型定义相等，所以 rw
策略可以再次完美匹配证明中的模式 (L2 n).length
。Leanstral 完成了任务，并向用户完美解释了理由。
关于程序的推理
我们从 https://www.cs.princeton.edu/courses/archive/fall10/cos441/sf/Imp.html 复制了 Rocq 中的定义，并要求 Leanstral 转换为 Lean。它成功完成了转换，甚至实现了自定义记法。示例片段：
inductive ceval : com → state → state → Prop where | E_Skip (st : state) : ceval .CSkip st st | E_Ass (st : state) (a1 : aexp) (n : Nat) (l : ident) (h : aeval a1 st = n) : ceval (.CAss l a1) st (update st l n) | E_Seq (c1 c2 : com) (st st' st'' : state) (h1 : ceval c1 st st') (h2 : ceval c2 st' st'') : ceval (.CSeq c1 c2) st st'' | E_IfTrue (st st' : state) (b1 : bexp) (c1 c2 : com) (h : beval b1 st = true) (h1 : ceval c1 st st') : ceval (.CIf b1 c1 c2) st st' | E_IfFalse (st st' : state) (b1 : bexp) (c1 c2 : com) (h : beval b1 st = false) (h1 : ceval c2 st st') : ceval (.CIf b1 c1 c2) st st' | E_WhileEnd (b1 : bexp) (st : state) (c1 : com) (h : beval b1 st = false) : ceval (.CWhile b1 c1) st st | E_WhileLoop (st st' st'' : state) (b1 : bexp) (c1 : com) (h1 : beval b1 st = true) (h2 : ceval c1 st st') (h3 : ceval (.CWhile b1 c1) st' st'') : ceval (.CWhile b1 c1) st st''
-- Notation for command evaluationnotation:50 c " / " st " ⇒ " st' => ceval c st st'
它也可以翻译为 Lean，然后在仅给出 Rocq 语句（不带证明）的情况下，证明该语言中程序的某些性质：
-- 示例命令：将变量 X 加 2
def plus2 : com := .CAss "X" (.APlus (.AId "X") (.ANum 2))
-- 定理：plus2 命令正确地将变量 X 加 2
-- 直觉：如果 X 在初始状态中的值为 n，执行 plus2 后，
-- X 在最终状态中的值将为 n+2
-- 这指定了 plus2 命令的行为
theorem plus2_spec (st : state) (n : Nat) (st' : state) (h1 : st "X" = n) (h2 : plus2 / st ⇒ st') : st' "X" = n + 2 := by
-- plus2 被定义为 .CAss "X" (.APlus (.AId "X") (.ANum 2))
-- 使用等式编译器展开它
change ceval (.CAss "X" (.APlus (.AId "X") (.ANum 2))) st st' at h2
cases h2 with
| E_Ass _ _ n l h =>
have : aeval (.APlus (.AId "X") (.ANum 2)) st = n := h
simp only [aeval] at this
rw [update]
simp [← this, h1]
需求证明。立即试用 Leanstral。
Leanstral 现已面向所有人开放使用。
Mistral Vibe 中的零设置：我们已将 Leanstral 直接集成到 Mistral Vibe 中，实现即时、零设置的 vibe 编码与证明。使用
/leanstall
来激活。然后要使用 Leanstral，请按 Shift+Tab
直到模型显示为 Leanstral，或者，使用 vibe --agent lean
。Labs API：通过我们的免费/近乎免费的 API 端点访问该模型
labs-leanstral-2603
。我们将在有限时间内保持该端点高度可访问，以收集真实反馈和可观测性数据，为下一代经过验证的代码模型提供动力。拥有权重：下载 Apache 2.0 许可的模型，并在你自己的硬件上运行。