Leanstral
我们首个为 Lean 4 设计的开源代码智能体，用于真实代码仓库中的形式化证明工程。119B 参数，激活 6.5B。
规格
- 上下文
- 262.1K
- 最大输出
- —
- 输入价
- —
- 输出价
- —
- 发布日期
- 2026-03-16
上下文
- 上下文
- 262.1K
- 最大输入
- —
- 最大输出
- —
价格
- 官方未公布
输入输出
- 输入
- 文本图像
- 输出
- 文本
API
- 接口类型
思考
- 官方未公布
源信息
- 状态
- 已下线
- 发布日期
- 2026-03-16
- 知识截止
- —
能力
- 已确认
调用方式
1 个 Provider
mistralmodel = labs-leanstral-2603
chat
POSThttps://api.mistral.ai/v1/chat/completions
JSON
标准格式
{
"id": "labs-leanstral-2603",
"object": "model",
"created": 1773619200,
"owned_by": "mistral",
"name": "Leanstral",
"api": {
"types": [
"chat"
]
},
"limits": {
"context": 262144,
"input": null,
"output": null
},
"modalities": {
"input": [
"text",
"image"
],
"output": [
"text"
]
},
"reasoning": {
"supported": null,
"efforts": []
},
"pricing": null,
"features": [
"tools",
"structured_output"
],
"info": {
"status": "retired",
"release_date": "2026-03-16",
"knowledge_cutoff": null,
"description": "Our first open-source code agent designed for Lean 4, built for formal proof engineering in realistic repositories. 119B parameters with 6.5B active.",
"docs": "https://docs.mistral.ai/models/leanstral-26-03",
"verified_at": "2026-10-11"
}
}官方来源
3