Leanstral：面向可信赖“氛围编程”的开源基础模型

AI 智能体已被证明是极具能力的代码生成工具。然而，当我们将这些模型推向高风险领域，从前沿数学研究到关键任务软件时，却遇到了一个扩展瓶颈：人类审查。手动验证所需的时间与专业知识成为工程速度的主要阻碍。

我们设想新一代更得力的编程智能体，既能完成编码任务，又能严格对照规范正式证明其实现的正确性。人们只需描述需求，不再需要调试机器生成的逻辑。今天，我们迈出了实现这一愿景的第一个重要步骤。

推出 Leanstral

我们发布 Leanstral，这是首个为 Lean 4 设计的开源代码智能体。Lean 4 是一种证明助手，既能表达复杂的数学对象，例如 perfectoid spaces，也能描述软件规范，例如 Rust 片段的行为。与现有作为大型通用模型包装器或仅专注于单一数学问题的证明系统不同，Leanstral 设计得高度高效（仅 60 亿活跃参数），并且专为在真实形式化仓库中运行而训练。

• 开放且可获取：我们以 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 仅需单次尝试（pass@1）就超越了它们。

即便是图中最强的开源竞争者 Qwen3.5-397B-A17B，也需要 4 次尝试（pass@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 版本变更的 Stack Exchange 帖子

当新版本的 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 evaluation

notation:50 c " / " st " ⇒ " st' => ceval c st st'

它还可以翻译成 Lean，然后在仅给出 Rocq 陈述（不带证明）的情况下，证明该语言中程序的一些属性：

-- 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 := -- 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 rename_i h have : aeval (.APlus (.AId "X") (.ANum 2)) st = n := h simp only [aeval] at this

要求证明。立即试用 Leanstral。

Leanstral 今日起面向所有人开放使用。

• Mistral Vibe 零配置：我们已将 Leanstral 直接集成到 Mistral Vibe 中，以实现即时、零配置的“氛围编程”与证明。使用 /leanstall 激活。之后按 Shift+Tab 直到模型显示为 Leanstral，或者使用 vibe --agent lean。

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

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

文档 - 注册 Mistral Vibe

AI agents have proven to be highly capable tools at code generation. Yet, as we push these models to high-stakes domains, ranging from frontier research mathematics to mission-critical software, we encounter a scaling bottleneck: the human review. The time and specialized expertise required to manually verify become the primary impedance of engineering velocity.

We envision a more helpful generation of coding agents to both carry out their tasks and formally prove their implementations against strict specifications. Instead of debugging machine-generated logic, humans dictate what they want. Today, we are taking the first major step toward that vision.

Introducing Leanstral

We release Leanstral, the first open-source code agent designed for Lean 4. Lean4 is a proof assistant capable of expressing complex mathematical objects such as perfectoid spaces and software specifications like properties of Rust fragments. Unlike existing proving systems that act as wrappers around large generalist models or focus on single math problems, Leanstral is designed to be highly efficient (with 6B active parameters) and trained for operating in realistic formal repositories.

• Open and accessible: We release Leanstral weights under an Apache 2.0 license, in an agent mode within Mistral vibe, and through a free API endpoint. We will also release a tech report detailing our training approach, and a new evaluation suite FLTEval, to move evaluations beyond their focus on competition math.

• Efficient and mighty: We use a highly sparse architecture for Leanstral, and optimise it for proof engineering tasks. Leveraging parallel inference with Lean as a perfect verifier, Leanstral is both performant and cost-efficient against existing closed-source competitors.

• Upgradable via MCP: Leanstral supports arbitrary MCPs through vibe, and was specifically trained to achieve maximal performance with the frequently used lean-lsp-mcp.

Evaluation

To reflect usefulness in realistic proof engineering scenarios, we benchmark Leanstral for completing all formal proofs and correctly defining new mathematical concepts in each PR to the FLT project, instead of isolated mathematical problems. We compare Leanstral against leading coding agents (Claude Opus 4.6, Sonnet 4.6, Haiku 4.5) and open-source models (Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B, GLM5 744B-A40B).

Leanstral vs. OSS Models

Leanstral-120B-A6B demonstrates a significant efficiency advantage over its much larger open-source peers. While models like GLM5-744B-A40B and Kimi-K2.5-1T-32B struggle to scale, capping their FLTEval scores at approximately 16.6 and 20.1 respectively, Leanstral outperforms them both with just a single pass.

Even Qwen3.5-397B-A17B, the strongest OSS competitor shown, requires 4 passes to reach a score of 25.4. In contrast, Leanstral achieves a superior score of 26.3 with half that investment (pass@2) and continues to scale linearly, reaching 29.3 at the same cost level.

Leanstral vs. Claude Family

Leanstral serves as a high-value alternative to the Claude suite, offering competitive performance at a fraction of the price: Leanstral pass@2 reaches a score of 26.3, beating Sonnet by 2.6 points, while costing only $36 to run, compared to Sonnet’s $549. At pass@16, Leanstral reaches a score of 31.9, comfortably beating Sonnet by 8 points. While Claude Opus 4.6 remains the leader in quality, it carries a staggering cost of $1,650, 92 times higher than running Leanstral.

In our benchmarking, we used Mistral Vibe as the scaffold with no modifications specifically for the evaluation.

Model	Cost ($)	Score
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

Case studies

Answering stackexchange posts about changes in newest Lean version

When breaking changes hit a new Lean release, migrating code can be a massive headache. We fed Leanstral a real-world question from the Proof Assistants Stack Exchange about a script that mysteriously stopped compiling in Lean 4.29.0-rc6 (which we did not train with due to its recency). The culprit was a rewrite (rw) tactic that suddenly failed to match patterns involving a simple type alias, initially written as def T2 := List Bool.

Instead of taking a stab in the dark, Leanstral rolled up its sleeves. It successfully built test code to recreate the failing environment and diagnosed the underlying issue with definitional equality. The model correctly identified that because def creates a rigid definition requiring explicit unfolding, it was actively blocking the rw tactic from seeing the underlying structure it needed to match.

The fix it proposed was simple: just swap def for abbrev. Because abbrev creates a transparent alias that is immediately definitionally equal to the original type, the rw tactic could once again perfectly match the pattern (L2 n).length in the proof. Leanstral completes the job and explains the rationale to the user perfectly.

Reasoning about programs

We copied over definitions in Rocq from https://www.cs.princeton.edu/courses/archive/fall10/cos441/sf/Imp.html and asked Leanstral to convert to Lean. It did so successfully, even implementing custom notation. Example snippet:

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'

It could also translate to Lean and then prove some properties about programs in this language when just given the Rocq statement (without proof):

-- 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') :

 -- 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

   have : aeval (.APlus (.AId "X") (.ANum 2)) st = n := h

   simp only [aeval] at this

Demand Proof. Try Leanstral Today.

Leanstral is available today for everyone to use.

• Zero-Setup in Mistral Vibe: We’ve integrated Leanstral directly into Mistral Vibe for immediate, zero-setup vibe coding and proving. Use /leanstall to active. Then to use Leanstral press Shift+Tab until the model displays as Leanstral, Alternately, use vibe --agent lean.

• Labs API: Access the model via our free/near-free API endpoint labs-leanstral-2603. We are keeping this endpoint highly accessible for a limited period to gather realistic feedback and observability data to fuel the next generation of verified code models.

• Own the Weights: Download the Apache 2.0 licensed model and run it on your own metal.

Documentation - Sign Up for Mistral Vibe