Home
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.

Modalities
Context
256k
Deprecation date5/22/2026

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

Mistral Medium 3.5 icon

Mistral Medium 3.5

v26.04
Voxtral TTS icon

Voxtral TTS

v26.03
Mistral Small 4 icon

Mistral Small 4

v26.03