Home
Models
Try in playground ↗
Leanstral 1.5 icon
Compare
Cat
June 30, 2026
v1.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.

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

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