benchr
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.
| Field | Verified record |
|---|---|
| Focus | Formal verification |
| Architecture | 119B total / 6B active |
| License | Apache-2.0 |
| Provider results | PutnamBench 587/672; FATE-H 87; FATE-X 34 |
A useful evaluation ends at the checker
Build the test around artifacts your team can verify, not around a judge model. Start with theorems already accepted in your repository, hide the proof, and record whether Lean accepts the generated result without repair. Add deliberately false premises and underspecified statements: a safe workflow must reject or escalate them rather than manufacture a proof.
| Test slice | What to record | Pass condition |
|---|---|---|
| Known theorem | Accepted proof, retries, wall time | Checker accepts without hidden manual edits |
| Near-miss statement | Counterexample or refusal | Does not present an invalid proof as complete |
| Repository task | Imports, style, maintainability | Fits the project and survives review |
| Resource run | Hardware, quantization, latency | Meets the team's own operating envelope |
The deployment decision has unanswered fields
The release gives a model size, active-parameter count, license, free API access, and proof results. It does not turn those facts into a production serving recipe. Before self-hosting, document the exact weights, precision, inference engine, concurrency target, memory headroom, and the Lean version used by the evaluation. Before using the hosted trial, confirm retention, rate limits, and whether the service terms fit the codebase.
Who should shortlist it?
A formal-methods group with a maintained Lean corpus and an automated checker has the right feedback loop. A general software team looking for chat, copywriting, or broad code completion does not. The strongest reason to test Leanstral is not the headline score; it is that the output can be checked by the tool the work is written for.
What a defensible evaluation report contains
Publish the corpus version, Lean toolchain, prompt policy, retry limit, time budget, and the exact condition that counts as solved. Separate proofs accepted on the first attempt from proofs repaired by an engineer; the second number measures a collaborative workflow, not autonomous completion. Keep rejected outputs and checker messages because they show whether the failure was mathematical, syntactic, or caused by a missing import.
Report the serving setup beside the result. A run on the free API and a self-hosted quantized build are different experiments even when the model name matches. Record weight revision, precision, hardware, concurrency, and wall-clock time. If a provider figure is shown for context, label it as provider-reported and do not merge it with your internal pass rate.
The final decision should state where a human remains in the loop: selecting lemmas, reviewing generated tactics, approving repository changes, or handling a checker failure. That boundary is more useful than a universal score. It tells the next reviewer what the model actually removes from the workflow and what responsibility stays with the proof engineer.