模型介绍
中文整理模型名称
Leanstral 1.5 119B A6B
模型用途
Leanstral 1.5 是一个开源代码代理模型，专为 Lean 4 设计。Lean 4 是一个证明助手，能够表达复杂的数学对象（如完美oid空间）以及软件规范（如 Rust 代码片段的属性）。
主要能力
基于 Mistral Small 4 系列构建，结合了多模态能力和高效架构。架构特点包括：MoE（混合专家）结构，128 个专家模块，每个 token 激活 4 个；模型总参数 119B，每个 token 激活 6.5B；支持 256k token 的上下文长度；支持多模态输入（文本和图像），输出文本。
推荐设置
温度（Temperature）：1.0
推理强度（Reasoning Effort）："none" 表示不使用推理，"high" 表示使用推理（推荐用于复杂提示词）
上下文长度：建议不超过 200k tokens
基本用法
安装 Mistral Vibe CLI 后，在终端输入 vibe --agent lean 命令启动（确保终端顶部显示 Leanstral）。建议在 VS Code 终端中运行，以便同时查看 vibe 和代码。建议在 Lean 项目目录中运行。可使用 /leanstall 命令安装 Leanstral。可以通过 API 调用或本地 vLLM 服务器使用该模型。
许可证
本模型基于 Apache 2.0 许可证发布。不得以侵犯、挪用或以其他方式违反第三方权利（包括知识产权）的方式使用本模型。
优先采用原作者提供的中文模型卡片；仅有英文说明时由闲社AI翻译整理。重要参数、许可证和商用范围请以原文为准。
你将获得什么
完整仓库方式包含该固定版本中的权重、配置、分词器及说明文件；指定版本方式只下载所选文件或整组分片。多模态模型的投影文件、配置等依赖，请按作者说明配齐。
完整仓库可能包含多个权重格式，因此需要的磁盘空间可能大于单一格式的模型大小。下载文件不等于完成模型部署。
使用前须知
运行模型需要的设备、工具与依赖，以原作者说明为准。
是否允许商用、修改和分发，请查看模型许可证。
闲社提供资料与镜像下载方法，不代表已运行模型或完成安全审计。下载的代码应先检查，再执行。
资料或下载有问题？
登录后可提交反馈。