Leanstral 1.5 119B A6B

Leanstral 1.5 119B A6B

Mistral 为 Lean 4 证明助手推出的开源代码智能体模型。它能证明定理、修复 Lean 代码，支持文本和图像，可通过 Mistral API 或你自己的 vLLM 服务器运行。

由 mistralai 在 Hugging Face 上制作。这些说明是 Mindket 根据它的模型页面和模型卡写的，模型自己的文件和许可证在 Hugging Face 上。

简介

它是什么：Leanstral 1.5 是开放权重的代码智能体模型，面向 Lean 4。Lean 4 是一个证明助手，既能表达高等数学，也能表达软件的规约。它属于 Mistral Small 4 系列，是早先 Leanstral 版本的更新。

它是混合专家模型，有 128 个专家，每个标记激活 4 个，总共 1190 亿个参数，其中 65 亿个处于激活状态。上下文长度是 256k 标记。它接受文本和图像，输出文本。

适合谁：适合想要一个能在项目里证明定理或修复代码的 AI 智能体的 Lean 4 用户，以及围绕 Lean 构建智能体的开发者。

Industry | Who uses it | How they use it | Example
数学 | Lean 用户和数学家 | 让智能体尝试证明给定的定理 | 在 Lean 项目里证明一个引理
软件验证 | 验证工程师 | 编写和修复形式化规约 | 修复规约里失败的证明
AI 智能体 | 智能体开发者 | 通过 MCP 把模型和 Lean 工具搭配使用 | 把模型接到 lean-lsp-mcp
教育 | 学生 | 获得 Lean 练习的帮助 | 让智能体补全一个证明步骤

如果你不用 Lean 4，可以跳过它，因为这个模型是为那个证明助手打造的。

用在哪里：

• Mistral Vibe 命令行工具，在你的 Lean 项目目录里运行。
• VS Code 的终端，模型卡建议这样做，让 vibe 和你的代码并排显示。
• 你自己的 vLLM 服务器，如果你不想调用 Mistral API。
• lean-lsp-mcp 工具，模型卡建议在配合 Lean 工作的智能体里使用它。

Use case | Who | What they get back
定理证明 | Lean 用户 | 对你给出的定理的证明尝试
代码修复 | 开发者 | 对你项目里 Lean 代码的修复
长任务 | 研究人员 | 对一个难题持续数小时的自主工作

如何设置：你需要完成 Mistral 账号设置，或者有一台本地 vLLM 服务器。

• 一个 Mistral 账号。免费套餐就够，需要在隐私设置里开启 Labs 模型
• 一个 Mistral API 密钥
• 按 Mistral 自己的指南安装 Mistral Vibe 命令行工具
• 一个用来工作的 Lean 4 项目

1. 登录你的 Mistral 账号，并开启 Labs 模型选项。
2. 创建一个 API 密钥。
3. 安装 vibe 命令行工具。
4. 启动 vibe，它会要你的密钥。如果没有，就运行设置命令。
5. 在 vibe 里输入 Leanstral 的安装命令，然后退出。

vibe --setup

在 vibe 里依次输入这两行：

/leanstall
exit

如何使用：在你的 Lean 项目里打开终端，启动 Lean 智能体。确认顶部显示的是 Leanstral。推荐的设置是温度 1.0，上下文不超过 200k 标记。

vibe --agent lean

如果要自动批准模型的改动，加上 yolo 参数，并且要小心使用：

vibe --agent lean --yolo

Tool | What it does
vibe --setup | 如果设置没有自动运行，就向你要 Mistral API 密钥
/leanstall | 在 vibe 里安装 Leanstral
vibe --agent lean | 启动 Lean 智能体
--yolo | 不再询问就批准模型的改动
lean-lsp-mcp | 让智能体能和 Lean 对话的工具

示例：在你的 Lean 项目文件夹里启动智能体，让它证明你写好的定理，或者修复一个出问题的证明。它可以对一个难题连续工作数小时，然后报告它改了什么。

新手与专家：如果你刚接触 Lean，先读一个简短的证明，再让智能体解释或扩展它。保持默认的批准提示开启，这样你能看到每一处改动。

对专家来说，推理强度设置有两个值：none 关闭推理，high 在复杂提示词时开启推理。本地 vLLM 方案需要 vllm 0.24.0 或更高版本，以及 vibe 智能体文件夹里的自定义智能体文件。模型卡建议在本地服务效果不好时改用 Mistral API。

你打开一个 Lean 4 项目
用 lean 智能体启动 vibe
Leanstral 读取你的文件和目标
它做一个证明或修复
你审查它做出的改动

注意事项：下面几点说明了限制和成本。

• Reasoning: 复杂提示词用 high，要跳过推理就用 none。
• License: Apache 2.0。
• Cost to run: 托管路线需要 Mistral API 密钥，模型卡说免费套餐就够。本地服务器需要大量 GPU 容量。
• Data it reaches: 除非你运行自己的 vLLM 服务器，否则你的项目文件和提示词会发送到 Mistral API。智能体配置还给了它一个 shell 工具。
• Not for: 不小心地自动批准改动，或 Lean 4 以外的工作。

Hugging Face 上的数据（2026年11月13日）

• 框架：vllm
• 最近 30 天下载：425
• 点赞：234
• 许可证：apache-2.0
• 基于：mistralai/Leanstral-2603
• Quantized versions: 15
• Fine-tunes: 2
• 标签：vllm

链接

• 模型：https://huggingface.co/mistralai/Leanstral-1.5-119B-A6B
• 文件：https://huggingface.co/mistralai/Leanstral-1.5-119B-A6B/tree/main

获取模型

用 Hugging Face 的命令行下载它的文件：

pip install -U huggingface_hub
hf download mistralai/Leanstral-1.5-119B-A6B

然后按它的模型卡使用它。这个工具包里没有会自己运行的东西。