AI 智能体已被证明是非常强大的代码生成工具。然而，当我们把这些模型推向高风险领域，从前沿数学研究到关键任务软件时，会遇到一个扩展瓶颈：人工审查。手动验证所需的时间和专业知识，成为工程效率的主要阻力。
我们设想有一代更有用的编码智能体，既能完成任务，又能依据严格的规约对自己的实现进行形式化证明。人类不必再调试机器生成的逻辑，只需说明自己想要什么。今天，我们朝着这一愿景迈出了第一大步。
Leanstral 登场
我们发布了 Leanstral，这是首个为 Lean 4 设计的开源代码智能体。Lean 4 是一种证明助手，能够表达诸如perfectoid 空间这样复杂的数学对象，以及Rust 代码片段的性质这类软件规约。现有的证明系统要么是通用大模型的封装，要么专注于单个数学问题，与之不同，Leanstral 被设计得极为高效（激活参数仅 6B），并经过训练，可在真实的形式化代码仓库中工作。
- 开放且易用：我们以 Apache 2.0 许可证发布 Leanstral 的权重，提供 Mistral vibe 中的智能体模式，并开放免费的 API 端点。我们还将发布一份详述训练方法的技术报告，以及一套新的评测集 FLTEval，让评测不再局限于竞赛数学。
- 高效且强大：Leanstral 采用高度稀疏的架构，并针对证明工程任务进行了优化。借助并行推理，并以 Lean 作为完美的验证器，Leanstral 与现有闭源竞品相比，性能出色且成本高效。
- 可通过 MCP 升级：Leanstral 通过 vibe 支持任意 MCP，并专门针对常用的 lean-lsp-mcp 做了训练，以获得最佳性能。
评测
为了反映在真实证明工程场景中的实用性，我们没有使用孤立的数学问题，而是以完成 FLT 项目每个 PR 中的全部形式化证明并正确定义新的数学概念，来对 Leanstral 做基准测试。我们将 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 仅用一次通过（single pass）就超过了它们两者。
即使是图中最强的开源对手 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 没有盲目乱试，而是撸起袖子干了起来。它成功构建了测试代码来重现失败的环境，并诊断出定义等价（definitional equality）方面的根本问题。模型正确地指出：由于 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 evaluation
notation:50 c " / " st " ⇒ " st' => ceval c st st'
只给出 Rocq 的命题陈述（不含证明），它还能将其翻译成 Lean，并证明这门语言中程序的一些性质：
-- Example command: adds 2 to variable X
def plus2 : com := .CAss "X" (.APlus (.AId "X") (.ANum 2))
-- Theorem: The plus2 command correctly adds 2 to variable X
-- Intuition: If X has value n in the initial state, after executing plus2,
-- X will have value n+2 in the final state
-- This specifies the behavior of the plus2 command
theorem plus2_spec (st : state) (n : Nat) (st' : state) (h1 : st "X" = n) (h2 : plus2 / st ⇒ st') :
st' "X" = n + 2 := by
-- plus2 is defined as .CAss "X" (.APlus (.AId "X") (.ANum 2))
-- Use equation compiler to unfold it
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 许可的模型，在你自己的硬件上运行。