Leanstral 1.5: Proof Abundance for All
Mistral AI has released Leanstral 1.5, a 7-billion parameter model specialized in generating proofs for the Lean theorem prover. Building on the previous version, it significantly boosts proof completion rates and offers a more accessible way for developers and mathematicians to use automated reasoning.
Background
- Mistral AI is a French company that builds large language models (LLMs) competing with OpenAI, Google, and Meta. Their models are known for being open-weight and efficient.
- Leanstral is a specialized version of Mistral's models fine-tuned to generate formal proofs for the Lean theorem prover — a software tool that checks mathematical reasoning at the level of each logical step.
- Formal proof systems like Lean are used to verify critical software (e.g., operating systems, compilers) and to give mathematicians absolute certainty about proofs too complex to check by hand. However, writing proofs in Lean is slow and requires rare expertise.
- This release (Leanstral 1.5) claims to produce dramatically more correct proofs than its predecessor, bringing AI-assisted formal verification closer to practical, everyday use. The "proof abundance" in the title refers to making formal proofs plentiful and accessible rather than scarce and expensive.