Mistral Releases Leanstral 1.5: Open Formal-Verification Model for Lean 4

Mistral

Research official 1 src. ~1 min

Mistral released Leanstral 1.5, a 119B total / 6B active MoE model specialized for formal mathematical proof engineering in Lean 4, under Apache-2.0 license. It saturates miniF2F (100%), solves 587/672 PutnamBench problems, and sets new SOTA on FATE-H (87%) and FATE-X (34%). In practical testing across 57 open-source repositories it discovered previously unknown bugs, including an integer overflow in a widely used zigzag decoding function.

Why it matters

First open-weight model to both saturate miniF2F and demonstrate real-world bug discovery at scale; Apache-2.0 licensing makes it directly deployable in commercial software-safety pipelines.

Importance: 4/5

SOTA on every formal-reasoning benchmark tested; first open-weight model to saturate miniF2F while finding real-world bugs in production code

mistral open-weights apache2 reasoning mathematics benchmark formal-reasoning

Sources

official Leanstral 1.5: Proof Abundance for All