# Leanstral 1.5 发布

- 来源：Hacker News 热门（buzzing.cc 中文翻译）
- 作者：vetronauta
- 发布时间：2026-07-01 09:46
- AIHOT 分数：40
- AIHOT 链接：https://aihot.virxact.com/items/cmr1frw1802hhslnli0u3w7ch
- 原文链接：https://docs.mistral.ai/models/model-cards/leanstral-1-5-26-06

## AI 摘要

Leanstral 1.5 是 Lean 4 形式证明工程模型的更新版，专为自动定理证明和自动形式化优化。总参数量 119B，激活参数 6.5B，上下文窗口 256k，免费使用。支持 Chat Completions、Function Calling、Agents、Structured Outputs、OCR、Embeddings 等 API 功能。

## 正文

Home

Models

Overview

Model Selection Guide

Best Practices

Prompting

Sampling

Deployment

Cloud

Self-Deployment

Labs

Try in playground ↗

Compare

June 30, 2026

Labs v 1.5

Leanstral 1.5

An updated Lean 4 formal proof engineering model optimised for automated theorem proving and autoformalization. 119B total parameters, 6.5B active.

labs-leanstral-1-5

Speed

Performance

Modalities

Context

i

256k

Price

i

$0

Speed

Performance

Modalities

Context

256k

Price

$0

FEATURES WEIGHTS

Features

Chat Completions /v1/chat/completions

Function Calling /v1/chat/completions/v1/conversations

Agents & Conversations /v1/agents/v1/conversations

Built-In Tools /v1/agents/v1/conversations

Structured Outputs /v1/chat/completions/v1/conversations

Predicted Outputs /v1/chat/completions/v1/conversations

Prefix /v1/chat/completions/v1/conversations

OCR /v1/ocr

Annotations - Structured /v1/ocr

BBox Extraction /v1/ocr

Document QnA /v1/chat/completions/v1/conversations

FIM /v1/fim/completions

Embeddings /v1/embeddings

Moderations /v1/moderations

Chat Moderations /v1/chat/moderations

Transcriptions /v1/audio/transcriptions

Text to Speech /v1/audio/speech

Timestamps /v1/audio/transcriptions

Batching /v1/batch

Other Models

Other Models

### Mistral Medium 3.5 v 26.04 ### Voxtral TTS v 26.03 ### Mistral Small 4 v 26.03