Mistral releases 'Leanstral 1.5,' an AI for automated theorem proving, supporting Lean 4 proof work.
Mistral AI released ' Leanstral 1.5, ' an AI model that assists in the mechanical verification of mathematical proofs and the correctness of programs, on June 30, 2026. Leanstral 1.5 is a model optimized for automated theorem proving and automated formalization for the formal proofing tool '
Leanstral 1.5 - Mistral AI | Mistral Docs
https://docs.mistral.ai/models/model-cards/leanstral-1-5-26-06
Mistral ships Leanstral 1.5 for Lean 4 proof work, free in Labs | AI Weekly
https://aiweekly.co/alerts/mistral-ships-leanstral-15-for-lean-4-proof-work-free-in-labs
Even if AI-generated text or code appears correct at first glance, it may contain subtle logical leaps or errors. In mathematical proofs and software verification, small mistakes can lead to major problems, so formal proof support systems like Lean 4 are used to demonstrate correctness in a way that computers can verify.
However, while formal proofs are convenient, their writing style is unique. Expressions that humans commonly use, such as 'obviously true' or 'can be proven in the same way,' are not understood by computers, and each step of the proof needs to be translated into a form that Lean 4 can understand. Converting natural mathematical text and specifications into descriptions suitable for Lean 4 is a time-consuming process, which is why dedicated AI models are needed to assist with automated theorem proving and automated formalization.
Leanstral 1.5 employs a mixed expert (MoE) architecture with a total of 119 billion parameters, where 6.5 billion parameters are active during processing. The context length is 256k tokens, allowing for the handling of long proof files and related code together. Leanstral 1.5 is the successor to the Leanstral released in March 2026, and the original March version was discontinued upon the release of Leanstral 1.5.
Mistral AI releases 'Leanstral,' an open-source proof verification platform for reliable AI coding, aiming to overcome the critical bottleneck of 'human review' - GIGAZINE
One of the applications of Leanstral 1.5, as indicated, is automated theorem proving, where AI assists in the process of proving a given proposition on Lean 4. For example, the developer inputs the goal of the proof, and Leanstral 1.5 then proposes the necessary proof steps, which are then verified by Lean 4.
Another application, automated formalization, involves converting human-readable mathematical explanations and specifications into a format that can be handled by Lean 4. Since excerpts from research papers or software specifications cannot be used directly for verification, they need to be rewritten into definitions and theorems that Lean 4 can understand. By reducing the burden of this conversion process, Leanstral 1.5 has the potential to extend formal proofs beyond specialists to practical verification work.
Leanstral 1.5 can be tried for free in the Mistral AI playground. It also supports API features such as 'Chat Completions,' 'Function Calling,' and 'Agents & Conversations.'
The model card does not include any new benchmarks showing how much performance has improved since the March version. AI Weekly, which reported on the release of Leanstral 1.5, also stated that it has not yet been able to confirm any new comparison results or policies regarding the release of weights.
Related Posts:
in AI, Posted by log1d_ts