leanstral formal proof agent.md

前言：为什么形式化证明在 2026 年突然变得重要

2026 年的 AI 编程领域正处于一个微妙的转折点。

一方面，代码生成模型已经强大到令人惊叹——从 Cursor 到 Codex，从 Claude Code 到 Mistral Vibe，AI 已经可以在数分钟内完成人类开发者需要数小时的编码任务。另一方面，一个越来越尖锐的矛盾开始浮现：AI 生成代码的速度远远超过了人类审查代码的速度。

这不是一个可以忽视的问题。当 AI 每小时产出数千行代码，而人类 reviewer 仍然以相同的速度逐行审查时，整个软件开发流水线的瓶颈已经从”写代码”转移到了”验证代码”。在普通业务代码中，这个问题或许还能用测试套件和 CI/CD 缓解；但在高风险场景——数学证明的正确性、金融系统的合规性、安全关键软件的无缺陷保证——“大概对就行”是不可接受的。

Mistral 在 2026 年 3 月 16 日发布的 Leanstral 正是对这个问题的一次系统性回答。它不是又一个通用代码生成模型，而是第一个专门为 Lean 4 形式化证明设计的开源 Agent。它的核心主张是：让 AI 不仅写代码，还能形式化证明自己写的代码是对的。

但 Leanstral 真正让人兴奋的，不仅仅是它在某个 benchmark 上的分数。它揭示了一条可能改变 AI 工程实践的范式路径——专精小模型 + 完美验证器 + 并行搜索。这条路径的效率曲线，是本文分析的重点。

一、背景知识：Lean 4 与形式化验证

1.1 什么是形式化验证

形式化验证（Formal Verification）是用数学方法严格证明软件或数学命题正确性的技术。与传统的单元测试不同，测试只能证明”在测试覆盖的场景下没有发现错误”，而形式化验证可以证明”在所有可能的输入下，程序的行为都符合规范”。

打一个比方：如果单元测试是”在 100 个随机点检查桥梁的承重能力”，那么形式化验证就是”用力学理论证明这座桥在任何荷载条件下都不会坍塌”。前者是经验性的，后者是数学性的。

1.2 Lean 4：不只是证明助手

Lean 4 是由微软研究院的 Leonardo de Moura 主导开发的依赖类型编程语言（dependently typed programming language），兼具两个身份：

• 编程语言：可以写真正能运行的程序，语法和功能接近 Haskell、Rust 等现代函数式语言
• 证明助手：可以在同一个框架内表达并验证数学定理和程序性质

这种双重身份赋予了 Lean 4 独特的优势。传统的证明助手（如 Coq、Isabelle）往往更偏向理论，写出来的”代码”主要用于证明目的，很难直接用于生产环境。而 Lean 4 的设计哲学是让证明和编程融为一体：你可以在同一个文件中定义数据结构、实现算法，然后证明这个算法的正确性。

Lean 4 生态中最重要的项目是 Mathlib——一个社区驱动的数学形式化库，已经包含了大量本科和研究生水平的数学定义和定理。截至 2026 年初，Mathlib 已有超过 200 万行代码，是世界上最大的统一数学形式化资源之一。

1.3 FLT 项目：费马大定理的形式化

本文多次提到的 FLT 项目（Fermat’s Last Theorem formalization）是由 Imperial College London 的 Kevin Buzzard 教授领导的大型开源项目，目标是在 Lean 4 中形式化证明费马大定理。该项目获得了 EPSRC 的资助（编号 EP/Y022904/1），计划持续到 2029 年。

费马大定理的证明涉及极其深奥的代数几何和数论知识（椭圆曲线的模性、Galois 表示的变形理论等），是对形式化验证工具能力的极限测试。Mistral 选择 FLT 项目作为评测基础，本身就说明了他们对 Leanstral 能力的信心。

1.4 之前的 AI + 形式化证明方案

在 Leanstral 之前，AI 辅助形式化证明已经有了一些探索：

• AlphaProof（DeepMind，2024）：在 IMO 2024 上获得金牌水平的表现，但聚焦于竞赛数学单题，不针对工程化的证明开发
• LeanDojo（2023）：开源的 Lean 交互环境和数据集，主要用于训练基础模型的 tactic 预测能力
• 通用大模型直接应用：将 Claude、GPT 等模型直接用于 Lean 代码生成，效果有限且成本极高
• ReProver、LeanCopilot 等：学术性质的证明搜索工具，专注于 tactic 级别的建议

这些方案的共同局限是：要么专注于竞赛数学的单题求解（与真实 proof engineering 工作流差距巨大），要么只是将通用模型包装了一层 Lean 接口（缺乏领域特化训练）。

Leanstral 的定位与上述方案不同——它是第一个专门训练的、面向真实仓库级 proof engineering 工作流的模型。

二、架构深度分析

2.1 稀疏混合专家（Sparse MoE）

Leanstral 采用稀疏 Mixture-of-Experts（MoE）架构，与 Mixtral 系列同源：

128 个专家，每 token 只激活 4 个——这意味着模型的”知识总量”很大（119B 参数覆盖了丰富的语言和数学知识），但每次推理的计算成本极低（只需要激活 6.5B 参数，相当于一个中小型模型的计算量）。

这种架构选择对于形式化证明任务具有特殊意义。证明任务的特点是需要深厚的知识储备但单步推理不需要巨大计算量：模型需要”知道”大量数学定义和引理（需要大参数量的知识存储），但生成每一步 tactic 的计算并不比写普通代码更复杂（不需要巨大的每 token 计算量）。MoE 架构恰好满足了”大知识、小计算”的需求。

2.2 基于 Mistral Small 4 家族

根据 HuggingFace 模型卡的描述，Leanstral 是 Mistral Small 4 家族的成员。这意味着它的底座模型继承了 Mistral Small 4 的通用能力——包括多语言支持（英法西德意葡荷中日韩阿拉伯语）、图像理解、函数调用、结构化输出等。

在此基础上，Leanstral 针对 Lean 4 proof engineering 进行了专门的训练优化。虽然 Mistral 尚未发布完整的技术报告（仅表示”将会发布”），但从模型表现可以合理推断，训练过程至少包括：

1. Lean 4 代码和证明的专项微调：大量 Mathlib、FLT 等真实 Lean 项目的代码作为训练数据
2. Agentic 工作流训练：训练模型在真实仓库环境中工作——理解文件结构、处理依赖关系、与工具交互
3. MCP 工具使用训练：专门优化了与 lean-lsp-mcp（Lean 语言服务器）的交互能力
4. 推理能力强化：支持 reasoning_effort 参数，可选择是否启用扩展推理

2.3 推理模式与温度设置

Leanstral 的推荐设置值得注意：

• 温度 = 1.0：这是一个相当高的温度值。对于通用代码生成任务，通常推荐 0.0-0.3 的低温度以获得确定性输出。但对于形式化证明，高温度 + 多次采样（pass@k）的策略更优——因为 Lean 编译器提供了完美的验证机制，多样性比确定性更重要。
• reasoning_effort = “high”：启用扩展推理模式，适合复杂证明任务
• 上下文长度建议 ≤ 200k：虽然支持 256k，但推荐不超过 200k 以保证质量

这些设置背后的哲学是：不追求单次完美，而是通过高多样性采样 + 外部验证来找到正确答案。

三、核心创新：完美验证器范式

3.1 为什么形式化证明是 AI 的”甜蜜点”

这是理解 Leanstral 效率优势的关键。

传统代码生成面临一个根本性困难：缺乏可靠的自动验证手段。你生成了一段代码，怎么知道它是对的？

• 单元测试？覆盖率有限，而且测试本身也可能有 bug
• 代码审查？依赖人类专家，速度慢且昂贵
• Reward Model？本身也是 AI，打分不一定准确

但形式化证明完全不同。Lean 编译器就是一个完美的验证器（Perfect Verifier）。

当你向 Lean 提交一个证明时，编译器会进行完整的类型检查（type checking）。如果编译通过，这个证明在数学意义上是绝对正确的——不是”大概率正确”，不是”在测试用例上正确”，而是经过逻辑推导链保证的、无条件正确的。如果编译不通过，你得到的是精确的错误信息，告诉你哪一步推导有问题。

没有模糊地带，没有误报，没有”false positive”。这是其他任何代码生成领域都不具备的性质。

3.2 完美验证器如何改变博弈规则

有了完美验证器，整个 AI 辅助证明的范式就从”追求单次正确率”变成了”最大化验证通过的概率-成本比”。

考虑这样一个对比：

场景 A：没有完美验证器的代码生成

• 大模型生成代码，单次正确率 80%
• 小模型生成代码，单次正确率 40%
• 你无法自动判断哪个是对的，必须人工审查
• 结论：用大模型更划算，因为减少了人工审查量

场景 B：有完美验证器的形式化证明

• 大模型生成证明，单次正确率 80%，成本 $10/次
• 小模型生成证明，单次正确率 40%，成本 $0.2/次
• Lean 编译器自动判断对错，零成本
• 小模型跑 5 次：至少一次通过的概率 = 1 - (0.6)^5 = 92.2%，成本 $1
• 小模型跑 10 次：至少一次通过的概率 = 1 - (0.6)^10 = 99.4%，成本 $2
• 结论：小模型 $2 达到 99.4$10 只有 80%

这就是为什么 Leanstral 能以 1/15 的成本超越 Claude Sonnet——不是因为它每次生成的证明质量更高，而是因为它够便宜，可以大量采样，而 Lean 保证了只要有一个对的就行。

3.3 从单次正确率到 pass@k 的思维跃迁

理解了完美验证器范式后，评价模型的标准也需要转变。传统的 pass@1（单次正确率）在这个范式下不再是最重要的指标，更重要的是在给定预算下的 pass@k 曲线形状。

这里有两个关键的数学性质：

性质 1：pass@k 的概率计算

如果模型的单次通过率为 p，则 k 次独立采样中至少有一次通过的概率为：

pass@k = 1 - (1-p)^k

性质 2：成本-成功率的关系

给定总预算 B 和单次推理成本 c，可采样次数 k = B/c，则：

success_rate(B) = 1 - (1-p)^(B/c)

这个公式揭示了一个反直觉的结论：在总预算固定的情况下，降低单次成本 c 比提高单次正确率 p 更有效——只要 p 不是太低。

举例：

• 模型 A：p=0.5, c=$10, 预算$100 → k=10 → success = 1-(0.5)^10 = 99.9%
• 模型 B：p=0.8, c=$100, 预算$100 → k=1 → success = 80%

模型 A 的单次正确率只有模型 B 的 62.5%，但在相同预算下成功率高出近 20 个百分点。这就是 Leanstral 的效率优势来源。

四、FLTEval：重新定义评测标准

4.1 为什么不用 MiniF2F

之前形式化证明领域最常用的 benchmark 是 MiniF2F——一组从 AMC/AIME/IMO 等数学竞赛中选取的题目，用 Lean（或 Isabelle）的形式化语言表述。

MiniF2F 的问题在于，它测试的是”解单题”能力，而真实的 proof engineering 是完全不同的工作流：

• 上下文依赖：你需要理解整个项目的结构——哪些引理已经证明了，哪些定义可以使用，哪些 tactic 在当前上下文中有效
• 定义新概念：不仅要证明定理，还要正确定义新的数学对象，这些定义会被后续证明依赖
• 版本兼容：真实项目使用特定版本的 Lean 和 Mathlib，模型需要适应不同版本的 API
• 工具交互：需要通过 LSP 查询类型信息、搜索已有引理、检查证明状态

用 MiniF2F 评测 Leanstral，就像用 LeetCode 面试题来评估一个人能不能在大型项目中工作一样——覆盖不了真实能力。

4.2 FLTEval 的设计

FLTEval 基于 FLT 项目（费马大定理形式化）的真实 Pull Request 设计。每个评测任务要求模型：

1. 在真实仓库环境中工作：不是孤立的文件，而是一个有完整依赖结构的 Lean 项目
2. 完成 PR 中所有形式化证明：不是一个证明，而是一组相关的证明
3. 正确定义新的数学概念：一些 PR 包含新的 def、structure、class 定义，模型需要给出正确的形式化
4. 使用 Mistral Vibe 作为 scaffold：模型以 Agent 身份工作，可以使用工具查询环境信息

这种评测方式比 MiniF2F 难度大幅提升，但也更贴近真实使用场景。

4.3 评测方法论的注意事项

需要明确指出的是，FLTEval 是 Mistral 自建的 benchmark。虽然他们承诺将开源评测套件，但在社区独立验证之前，我们需要保持审慎的态度。自家出题自家考，存在潜在的优化偏差：

• 训练数据可能与评测任务存在分布上的亲近性
• 评测的难度分布和题目选择可能无意中偏向模型的长处
• 竞品模型可能没有针对这类任务做过任何优化

不过，Mistral 在博客中明确表示竞品模型使用的是同样的 Mistral Vibe scaffold 和相同的运行环境，这在一定程度上保证了对比的公平性。

五、效率曲线：最具启发性的发现

5.1 核心数据

5.2 三条关键曲线

从这组数据中，可以提取出三条具有深刻启示的曲线：

曲线 1：通用大模型的”天花板效应”

GLM5（744B 总参数，40B 活跃）和 Kimi（1T 总参数，32B 活跃）在 FLTEval 上的表现分别停滞在 ~16.6 和 ~20.1。增加采样次数（pass@k）并不能显著提升它们的分数。

这意味着这些模型的错误不是”随机的”，而是”系统性的”——它们缺乏解决某类问题的知识或能力，多试几次也无济于事。就像一个不懂微积分的人，给他再多时间也算不出积分题。

曲线 2：Leanstral 的”线性增长”

Leanstral 的 FLTEval 得分随 pass@k 的增长呈现接近线性的增长趋势：

pass@1:  21.9
pass@2:  26.3  (+4.4)
pass@4:  29.3  (+3.0)
pass@8:  31.0  (+1.7)
pass@16: 31.9  (+0.9)

虽然边际收益在递减（符合概率论的预期），但直到 pass@16 仍然在持续增长，没有出现通用模型那样的硬顶效应。这说明 Leanstral 的错误主要是”随机的”——不是不会做，而是在多条可能的证明路径中没有恰好选中正确的那条。多采样几次，总能找到。

曲线 3：性价比的交叉点

最令人震撼的对比：

• Leanstral pass@2 ($36) vs Sonnet ($549)：Leanstral 以 1/15 的成本超出 2.6 分
• Leanstral pass@4 ($72) vs Sonnet ($549)：Leanstral 以 1/8 的成本超出 5.6 分
• Leanstral pass@16 ($290) vs Sonnet ($549)：Leanstral 以 1/2 的成本超出 8.2 分

但也要看到另一面：

• Leanstral pass@16 ($290) vs Opus ($1,650)：Opus 仍然领先 7.7 分

这意味着在”性价比”维度上，Leanstral 是无可争议的赢家；但在”不惜代价追求最高质量”的场景下，Opus 仍然是最强选择。

5.3 效率曲线的深层含义

这组曲线的启发性远超形式化证明这个特定领域。它揭示了一个普适性的 AI 工程原理：

当存在可靠的外部验证机制时，专精小模型 + 并行采样 + 验证过滤，几乎总是比通用大模型更具性价比。

这个原理可以推广到：

1. 代码生成 + 编译器/测试套件验证：用小模型大量生成代码候选，自动编译 + 跑测试，通过即可
2. 数学推理 + 符号计算验证：用小模型生成解题步骤，Mathematica/SymPy 自动验证
3. 数据分析 + 业务规则校验：用小模型生成 SQL/分析报告，自动化规则引擎验证输出
4. 硬件设计 + EDA 工具验证：用小模型生成 RTL 代码，综合工具自动验证

核心条件是：存在一个比 AI 生成更便宜、且判断绝对准确的验证器。Lean 编译器恰好是形式化证明领域最完美的验证器。

5.4 为什么通用大模型有天花板

通用大模型在形式化证明上的天花板效应值得深思。GLM5 有 744B 参数（40B 活跃），Kimi 有 1T 参数（32B 活跃），它们的训练数据覆盖了互联网上绝大多数文本，但在 Lean 4 形式化证明上的表现仍然远逊于 6.5B 活跃参数的 Leanstral。

可能的原因包括：

1. 训练数据稀缺：Lean 4 代码在互联网上的占比极低。Mathlib 虽然有 200 万行，但相比 Python/JavaScript 的海量代码，只是九牛一毛。通用模型在预训练中接触到的 Lean 代码太少，难以学到深层的 tactic 使用模式
2. 形式化推理的特殊性：Lean 证明需要精确的类型匹配和逻辑推导，容错空间为零。通用模型擅长的”模糊近似”能力在这里完全不适用
3. 工具交互的缺失：通用模型通常不针对 Lean LSP 交互做训练，无法有效利用 proof state 和类型查询
4. MoE 路由的低效：通用 MoE 模型的专家是按通用任务分配的，不存在”Lean 证明专家”。而 Leanstral 的专家分配可能已经针对证明任务做了优化

六、MCP 与 Agentic 工作流

6.1 MCP 集成

Leanstral 支持通过 MCP（Model Context Protocol） 接入外部工具，这是它区别于简单的”代码补全模型”的关键特性。MCP 是 Anthropic 提出的标准化协议，允许 AI 模型以结构化方式调用外部工具。

Leanstral 特别针对 lean-lsp-mcp 做了训练优化。通过 Lean 语言服务器的 MCP 接口，模型可以：

• 查询当前 proof state：了解还需要证明什么目标
• 查询类型信息：确认某个表达式的类型是否符合预期
• 搜索已有引理：在 Mathlib 的庞大库中找到可用的引理
• 检查定义展开：确认 def 和 abbrev 的行为差异
• 获取错误诊断：理解为什么某个 tactic 失败

这种交互式的工作方式比”一次性生成完整证明”强大得多。就像人类数学家在证明过程中会不断检查推导、翻阅参考书一样，Leanstral 也可以在证明过程中动态查询环境、调整策略。

6.2 Mistral Vibe 集成

Leanstral 的推荐使用方式是通过 Mistral Vibe（Mistral 的 CLI 编码 Agent 框架）。在 Vibe 中只需运行 /leanstall 命令即可配置 Leanstral——这会自动设置模型、系统提示词（LEAN.md）、以及子 Agent 支持。

从 LEAN.md 系统提示词可以看到 Mistral 对 Leanstral 工作流的详细设计：

• 三阶段流程：Orient（理解任务）→ Plan（制定计划）→ Execute & Verify（执行并验证）
• 读后写原则：不允许编辑未读过的文件
• 循环打破机制：同一区域尝试两次失败后必须切换策略，禁止”添加 X → 删除 X → 添加 X”的反复摇摆
• 不使用 sorry：除非用户明确要求，否则不允许留下未完成的证明
• 不自动 git commit：保留人类的最终审查权

这些设计体现了对真实工程实践的深刻理解——形式化证明不是学术游戏，而是需要严格流程管理的工程活动。

6.3 本地部署

Leanstral 支持通过 vLLM 本地部署：

vllm serve mistralai/Leanstral-2603 \
  --max-model-len 200000 \
  --tensor-parallel-size 4 \
  --attention-backend FLASH_ATTN_MLA \
  --tool-call-parser mistral \
  --enable-auto-tool-choice \
  --reasoning-parser mistral

需要注意的是，当前需要使用 Mistral 定制的 vLLM Docker 镜像（mistralllm/vllm-ms4:latest），因为主线 vLLM 尚未合并 Mistral 的工具调用和推理解析补丁。4 卡 GPU 并行推理，适合有 A100/H100 集群的研究团队自建。

七、真实案例深度分析

7.1 案例 1：诊断 Lean 版本升级 bug

这个案例来自 Proof Assistants Stack Exchange 的真实问题，提问者遇到了代码在 Lean 4.29.0-rc6 中突然编译失败的问题。

问题背景：

用户定义了 def T2 := List Bool，然后在证明中使用 rw 策略（rewrite tactic）对包含 T2 的表达式进行改写，在旧版本中正常工作，升级后失败。

Leanstral 的诊断过程：

1. 环境搭建：首先构建了测试环境来复现问题（注意：Lean 4.29.0-rc6 发布时间晚于训练数据截止日期，这说明模型在做泛化推理而非记忆）
2. 根因分析：诊断出核心问题——def 创建的是 rigid definition（不透明定义），需要显式 unfold 才能展开。当 Lean 内部的 unification 算法发生变化时，rw 策略无法自动看穿 def 定义来匹配模式
3. 修复方案：建议将 def T2 := List Bool 改为 abbrev T2 := List Bool
4. 原理解释：abbrev 创建的是透明别名（transparent alias），在定义等价（definitional equality）的意义上直接等于原始类型，因此 rw 可以直接匹配

技术深度解析：

这个案例展示了 Lean 类型论中一个微妙但重要的区别：

• def 在 Lean 4 中创建的定义默认是”不透明”的——kernel 不会自动展开它。这意味着 T2 和 List Bool 在某些推导上下文中被视为不同的类型
• abbrev 创建的是带有 @[reducible] 属性的定义，elaborator 和 unifier 会自动展开它

这种 def vs abbrev 的区别是 Lean 4 初学者经常踩的坑，即使有经验的用户在版本升级时也可能被绊倒。Leanstral 能准确诊断这类问题，说明它对 Lean 4 类型系统的理解不是表面的模式匹配，而是深入到了类型论层面。

7.2 案例 2：跨语言转译 + 性质证明

Leanstral 成功地将 Rocq（Coq 的后继者）中的程序定义翻译到 Lean 4，包括：

• 实现自定义 notation（Lean 4 的 notation 系统与 Rocq 差异很大）
• 将翻译后的程序进行性质证明——仅给 Rocq 的命题陈述（不给证明），由 Leanstral 自行在 Lean 中完成证明

这展示了模型不仅理解单一证明助手的语法，还能在不同形式化系统之间进行语义级别的翻译。

八、产业影响与更广泛启示

8.1 对 Lean 4 生态的加速效应

形式化证明社区一直是一个小众而精英的圈子。入门门槛极高（需要掌握类型论、逻辑学、以及 Lean/Coq/Isabelle 等工具的复杂语法），社区规模远小于主流编程语言。

Leanstral 的开源（Apache 2.0）+ 免费 API 可能显著改变这个局面：

• 降低入门门槛：新手可以通过 AI 辅助快速上手 Lean 4，不必独自面对陡峭的学习曲线
• 加速 Mathlib 贡献：更多开发者可以参与 Mathlib 的扩展，形成正反馈循环
• 推动 FLT 项目进展：Kevin Buzzard 团队可以利用 AI 加速费马大定理的形式化进程
• 吸引工业界注意：当形式化验证变得更容易、更便宜时，它在安全关键软件中的应用将显著扩大

8.2 “专精小模型”范式的验证

Leanstral 是”专精小模型”哲学的一个强有力案例。在 Scaling Law 驱动的”越大越好”叙事之外，它展示了另一条路径的可行性：

• 6.5B 活跃参数 > 17B-40B 活跃参数（在特定任务上）
• 训练数据的领域匹配度 > 参数规模
• 任务特化的训练方法 > 通用能力的溢出

这不是说大模型没有价值——Opus 仍然以 39.6 的绝对分数领先所有竞争者。但在成本敏感的场景下，专精小模型 + 领域适配可能是更明智的选择。

8.3 对 AI 安全的潜在影响

从长远来看，形式化验证 + AI 的结合可能对 AI 安全产生深远影响：

• 可验证的 AI 系统：如果关键的 AI 组件可以用形式化方法验证其正确性，我们就不必完全依赖经验性的测试和评估
• AI 对齐的形式化：理论上，某些对齐约束可以表述为形式化规范，然后用 Lean 等工具验证 AI 系统是否满足这些约束
• 可信 Agent：当 AI Agent 执行高风险操作时，如果它能提供形式化证明来证明其行为符合给定规范，将大大提高人类对 Agent 的信任度

当然，这些愿景距离实现还有很长的路。目前的形式化验证主要覆盖数学定理和特定语言规范（如通过 Aeneas 项目验证 Rust 代码的性质），离”验证任意程序的任意性质”还有巨大的鸿沟。

九、批判性分析

9.1 需要关注的风险

1. 自建 benchmark 的可信度：FLTEval 尚未被社区独立验证。虽然 Mistral 承诺开源，但在此之前我们只能把它当作”一家之言”。自家训练的模型在自家设计的评测上表现好，说服力天然打折扣。

2. 形式化证明的适用边界：目前 Leanstral 展示的能力主要集中在纯数学证明领域。从数学证明到”验证任意软件的正确性”之间的距离，可能比看起来大得多。现实世界的软件涉及 I/O、并发、网络通信、用户交互等复杂因素，形式化建模的难度远超纯数学。

3. Lean 4 生态的局限性：尽管 Mathlib 已经很大，但相比 Python/JavaScript 等主流语言的生态仍然很小。工具链成熟度、IDE 支持、社区资源都还有很大的提升空间。选择 Lean 4 作为形式化验证的主战场，意味着承担了生态建设的长期投入。

4. pass@k 的边际递减：虽然 Leanstral 的 scaling 曲线比通用大模型好得多，但从 pass@8 (31.0) 到 pass@16 (31.9) 的增量只有 0.9 分，边际收益在加速递减。这暗示在某个点之后，单纯增加采样次数也将触及天花板——更好的搜索策略（如 tree search、beam search）可能比暴力采样更有效。

5. 与 Opus 的差距：Opus (39.6) vs Leanstral pass@16 (31.9) 的 7.7 分差距不算小。在最高质量需求的场景下（比如验证安全关键系统），可能仍然需要使用昂贵的大模型。

9.2 被低估的亮点

1. 泛化能力的证据：在 Lean 4.29.0-rc6 的 bug 诊断案例中，模型处理的是训练数据截止之后的版本变更，表现出了真正的推理泛化能力，而非简单的记忆回放。

2. 跨系统翻译能力：Rocq → Lean 4 的转译不是简单的语法替换，而是需要理解两种不同类型论系统的语义差异。这种能力的实际工程价值可能比 benchmark 分数更大。

3. Apache 2.0 的战略意义：完全开源意味着企业可以基于 Leanstral 构建自己的形式化验证工具链，无需担心许可证限制。这可能催生一批垂直领域的形式验证创业公司。

4. MCP 支持的可扩展性：通过 MCP 接入外部工具的能力使得 Leanstral 不是一个封闭系统，而是一个可持续扩展的平台。随着 Lean 生态工具的丰富，Leanstral 的能力也会随之增长。

5. 推理模式（reasoning_effort）的灵活性：支持关闭推理（快速回答简单问题）和高推理（处理复杂证明）的切换，使得模型在不同场景下都能高效使用。

十、总结：一条值得认真对待的范式路径

Leanstral 不是一个在 benchmark 上刷分的学术项目，而是对一个深层次工程问题的系统性回答：当 AI 生成代码的速度远超人类审查速度时，我们如何保证正确性？

它给出的答案是：让代码自己证明自己的正确性，然后用数学工具验证这个证明。

这个答案的实用性目前还有限——形式化验证的适用范围远小于通用编程。但它展示的效率曲线具有普适性启发价值：

在任何存在可靠外部验证器的领域，专精小模型 + 并行采样 + 验证过滤，几乎总是比通用大模型更具性价比。

这不是一个理论推导，而是有真实数据支撑的结论：$36 vs$549，得分还更高。

对于关注 AI 工程实践的人来说，这条效率曲线值得反复品味。它指向的不仅仅是形式化证明的未来，而是整个 AI-assisted engineering 的一种可能演进方向——不追求单次完美，而是用廉价的多样性 + 可靠的验证来逼近正确性。

参考资料

• Mistral 官方博客：Leanstral: Open-Source foundation for trustworthy vibe-coding
• HuggingFace 模型卡：mistralai/Leanstral-2603
• Mistral 文档：Leanstral Model Documentation
• FLT 项目：Imperial College London / FLT
• Lean 4：leanprover/lean4
• Mathlib：leanprover-community/mathlib4
• Aeneas（Rust 形式化验证）：AeneasVerif/aeneas