Leanstral 1.5 is for proofs, not chat: read its benchmark claims in context
Leanstral is built for formal proofs. Its open weights and proof scores do not make it a general chat model.
By the benchr team · · Changelog · Provider-published facts rechecked against the official sources on July 28, 2026
MISTRAL · LEANSTRAL1.5FORMAL PROOF · OPEN
Benchr model field plateLeanstral 1.5Proof specialist · traceable route
Editorial imageA BenchR editorial illustration of specialist proof work: each conclusion should stay traceable to a controlled set of premises.
Total params119B6B active
LicenseApache2.0
PutnamBench587/672Mistral-reported
Released2 Jul2026
Leanstral 1.5 arrived July 2 with a narrow job: formal verification. That focus makes the model easier to judge, as long as you keep general chatbot expectations out of the comparison.
Read the proof scores as proof scores
Mistral reports 587 solved problems out of 672 on PutnamBench, along with FATE results. Those are provider-reported results in a proof domain. They can help a Lean team decide whether to test the model. They say nothing about marketing copy, customer support, or a general coding assistant.
119B total is not a hardware shopping list
Mistral describes 119B total parameters with 6B active. That matters for deployment planning, but it does not specify the machine you need. Quantization, serving stack, batch size, context policy, and target latency determine the practical footprint.
Open weights make testing easier, not optional
The Apache-2.0 license suits controlled environments, and Mistral says a free API is available. Build a proof corpus with checker-verified outcomes, adversarial counterexamples, and human review. A provider benchmark is enough to start the test, not to pass it.
benchr