AI 写代码已经不是新鲜事了。但写出来的代码到底能不能信？测试能跑、review 过了、fuzzing 没发现问题——这些都只能说明"看起来没问题"。
Mistral AI 在 7 月 2 日开源了 Leanstral 1.5。它能做的事是：你告诉模型你想要什么，它写出代码，然后给出数学证明，证明这段代码符合你的要求。证明由 Lean 4 编译器内核逐行检查，不会出错。
不是"希望代码能跑"，而是"证明代码一定正确"。
Leanstral 1.5 能做什么
从官方文档和模型卡来看，Leanstral 1.5 是一个专门针对 Lean 4 的形式化验证和代码证明模型，属于 Mistral Small 4 系列。核心能力包括：
数学定理证明。从初等数学到国际奥赛（miniF2F），从 Putnam 数学竞赛到研究生/博士级别的抽象代数（FATE-H/FATE-X），模型可以自动生成证明，不需要人工推导。
形式化代码验证。模型能证明实际代码实现的正确性——比如 AVL 树的 O(log n) 时间复杂度保证，需要结构归纳法、单子时间追踪和详尽的重新平衡情况分析。
自动化 Bug 发现。配合 Aeneas 工具链（Rust → Lean 翻译），模型可以把代码转换成形式化表示，推断代码意图、生成正确性属性、尝试验证或证伪。在 57 个开源仓库中发现了 11 个真实 bug，其中 5 个此前未被报告。
代码代理能力。模型可以在文件系统中像开发者一样工作——编辑文件、运行 bash 命令、使用 Lean 语言服务器实时检查编译目标和错误信息。支持工具调用（Function Calling），比如调用 lean_run_code 函数编译和运行 Lean 代码片段。
实际 PR 协作。FLTEval 基准来自 Fermat 的最后一个定理仓库的真实 PR，模型可以直接处理真实项目中的证明工作。
核心数据
以下全部来自官方资料：
-
• 架构：119B 总参数，MoE 混合专家，每 token 仅激活 6B 参数 -
• 许可：Apache 2.0 开源，HuggingFace 下载权重 + Mistral API 免费调用 -
• 上下文窗口：256K token（据 aiweekly.co 报道，官网未明确标注） -
• miniF2F：488 道奥赛级数学题，验证集和测试集全部满分 100% -
• PutnamBench：672 道 Putnam 数学竞赛题，解决 587 道，平均成本约 $4/题 -
• FATE-H：87%（硕士级抽象代数） -
• FATE-X：34%（博士级抽象代数） -
• FLTEval：pass@1 从 21.9 提升至 28.9，pass@8 从 31.9 提升至 43.2（超过 Opus 4.6 的 39.6，成本仅 1/7） -
• 代码验证：扫描 57 个开源仓库，发现 11 个真实 bug，其中 5 个此前未被报告 -
• 发布时间：2026 年 7 月 2 日，由 Mistral AI Leanstral 团队发布
形式化验证，终于普通人也能用了
Coq、Isabelle、Lean 这些证明辅助工具已经存在几十年，学术界一直在用。门槛极高——精通数学逻辑，熟悉证明辅助工具，手动推导每一步。Lean 社区有句话：写一个形式化证明的时间通常是写代码的十倍。
Leanstral 1.5 做的事是把推导交给 AI。
模型接收定理或代码规范，提交证明，收到 Lean 编译器的反馈——目标、错误、类型信息——然后不断修改直到成功或预算耗尽。整个过程自动化，不需要人类专家逐行推导。
两个实际案例
AVL 树时间复杂度证明
模型为一个真实的 AVL 树实现证明了 O(log n) 的插入/删除时间复杂度保证。跑了 270 万 token，22 次上下文压缩，最终建立每高度单位约 48 步加常数的时间上界。
Rust 代码溢出 Bug
datrs/varinteger 的符号函数在输入 Std.U64.MAX 时溢出。调试版本崩溃，发布版本静默损坏数据。这是 5 个此前未报告的 bug 之一。
训练方法
中间训练、监督微调、基于 CISPO 的强化学习，三阶段。
两个训练环境。多轮环境里，模型收到定理，提交证明，收到编译器反馈，修改直到成功。跟人类学数学一个逻辑：做错了看反馈，再试。
代码代理环境里，模型像开发者一样操作文件系统：编辑文件、跑 bash、用 Lean 语言服务器实时检查目标和错误。SafeVerify 验证结果。
PutnamBench 上的数据比较有意思。5 万 token 解决 44 题，20 万 244 题，100 万 493 题，400 万 587 题。一直涨，没见顶。
成本对比
FLTEval 基准上，Opus 4.6 的 pass@8 是 39.6。Leanstral 1.5 达到 43.2，官方称成本是后者的 1/7。
PutnamBench 每题 $4，Seed-Prover 1.5 high 约 $300 以上。
MoE 架构的原因：119B 总参数里每 token 只激活 6B，加上专门针对 Lean 4 训练，没有通用模型那种冗余计算。
适用场景和局限
适合的场景
-
• 数学定理的形式化证明——从初等数学到博士级别 -
• 自动化代码审计——Rust 项目配合 Aeneas 工具链
不适合的场景
-
• 日常代码编写——写 Python 脚本、前端页面、数据清洗等，这不是它的定位 -
• 通用对话或聊天——这不是对话模型
部署门槛
本地部署官方推荐 4 张 GPU。6B 激活参数是 MoE 架构——119B 总参数每 token 只激活 6B，但消费级单卡跑不动。
快速上手
Mistral Vibe 方式（官方推荐）
uv tool install mistral-vibe
uv tool update mistral-vibe
vibe --setup
vibe
/leanstall
exit
vibe --agent lean
本地部署（vLLM，需 4 卡）
uv pip install -U vllm --torch-backend=auto
vllm serve mistralai/Leanstral-1.5-119B-A6B \
--max-model-len 200000 \
--tensor-parallel-size 4 \
--attention-backend FLASH_ATTN_MLA \
--tool-call-parser mistral \
--enable-auto-tool-choice \
--reasoning-parser mistral
API 调用（Python）
from openai import OpenAI
client = OpenAI(api_key="EMPTY", base_url="http://localhost:8000/v1")
response = client.chat.completions.create(
model="mistralai/Leanstral-1.5-119B-A6B",
messages=[{"role": "user", "content": [
{"type": "text", "text": "Define the transition rules as an inductive proposition..."}
]}],
temperature=1.0,
max_tokens=32000,
reasoning_effort="high"
)
print("Content:", response.choices[0].message.content)
print("Reasoning:", response.choices[0].message.reasoning)
推荐参数：temperature 1.0，max_tokens 32000，reasoning_effort 选 none 更快、high 推理更深，auto_compact_threshold 168000。
相关链接：
-
• 官方公告：https://mistral.ai/news/leanstral-1-5/ -
• HuggingFace 模型：https://huggingface.co/mistralai/Leanstral-1.5-119B-A6B -
• Mistral Vibe 文档：https://docs.mistral.ai/models/leanstral-1-5