News · 2026-06-30

Mistral releases a lean, open model built for formal math proofs

Mistral AI released Leanstral 1.5, a specialized model that writes mathematically rigorous proofs checked by the Lean 4 proof assistant, guaranteeing correctness rather than plausibility. The open-weight, mixture-of-experts model has 119 billion total parameters but activates only about 6.5 billion per task, and carries a 250,000-word context window. Details are in Mistral's model card.

Key facts

• What: Leanstral 1.5 is a free, open model specialized for writing machine-checked mathematical proofs, using a design that keeps only a small slice of itself active at a time.
• When: 2026-06-30
• Primary source: read the source

Leanstral 1.5 is built for two closely related jobs, both centered on Lean 4. Lean is a proof assistant—software that checks mathematical proofs line by line and accepts an argument only if every step is airtight. Leanstral is tuned to write proofs in Lean's formal language and to perform autoformalization: taking ordinary human-written mathematics and translating it into the precise, machine-checkable form Lean demands.

This matters because it attacks the deepest weakness of ordinary AI models: they produce answers that sound right without any guarantee of being right. Ask a normal chatbot to prove a theorem and it will generate a fluent, authoritative-looking argument that may contain a fatal gap—the same fabrication problem covered in why does AI make things up. But if a model writes its proof in Lean, the proof assistant checks it mechanically. If Lean accepts it, the proof is correct with near-certainty; if there is a flaw, Lean rejects it. The AI cannot bluff its way past a machine checker. That turns math from something an AI merely asserts into something it can actually prove, and gives the model an automatic, unfakeable feedback signal to learn from.

Leanstral's design also exemplifies an important efficiency trend. It has about 119 billion total parameters but activates only around 6.5 billion for any given piece of work. This is the mixture-of-experts approach, explained in full in the lesson on mixture of experts: rather than run the entire giant model for every token, the system routes each step to a small, relevant subset of specialists. The result is a model with the knowledge capacity of something very large but the running cost of something much smaller. It also carries a context window of a quarter-million words, which matters for proofs since a formal argument can be long and every earlier step has to stay in view. The model is free and open, released through Mistral's platform, continuing the company's pattern of putting capable specialized models in the open rather than locking them behind a paywall; see open-weight models for why that choice shapes the field.

The honest caveat is that this is a narrow tool, and its narrowness is both its strength and its limit. Leanstral is not going to help you write an email or debug a web app; it is built for a specialized corner of mathematics and formal verification that most people will never touch directly. Formal proof, for all its rigor, is slow, demanding work—translating real mathematics into a form a machine will accept is famously laborious, which is exactly why an AI assistant for it is valuable, but also why progress here is measured in patient increments rather than viral demos. The broader significance is bigger than the model itself: as AI gets pushed into high-stakes domains where a plausible-but-wrong answer is dangerous, the ability to generate results that can be mechanically checked—rather than merely trusted—becomes one of the most valuable things a model can do. Leanstral is a small, concrete step toward AI whose math you do not have to take on faith.

Primary source, verified: read the paper →

Topics: Mistral · open-weight-models · formal-methods · mathematics · mixture-of-experts