Models
Try in playground ↗
Leanstral icon
Compare
Cat
March 16, 2026
v26.03

Leanstral

Our first open-source code agent designed for Lean 4, built for formal proof engineering in realistic repositories. 119B parameters with 6.5B active.

Speed
Performance
Modalities
Context
256k
Price
$0
Speed
Performance
Modalities
Context
256k
Price
$0

Features

Chat Completions
Function Calling
Agents & Conversations
Built-In Tools
Structured Outputs
Predicted Outputs
Prefix
OCR
Annotations - Structured
BBox Extraction
Document QnA
FIM
Embeddings
Moderations
Chat Moderations
Transcriptions
Text to Speech
Timestamps
Batching
Other Models

Other Models

Voxtral TTS icon

Voxtral TTS

v26.03
Mistral Small 4 icon

Mistral Small 4

v26.03
Mistral Large 3 icon

Mistral Large 3

v25.12