Leanstral 1.5 expands Mistral’s open proof-engineering model

Mistral released Leanstral 1.5 on July 2, updating its specialized model for formal proof engineering. The announcement provides Apache-licensed weights and opens the FLTEval evaluation suite. Mistral describes training both on repeated proof attempts with compiler feedback and on agent tasks involving files, commands, and a language server.

Longer attempts are part of the result

The company reports improvements on mathematical and repository-based evaluations, including experiments in which substantially larger inference budgets produce additional solved problems. It also describes a code-verification pipeline combining translation into Lean with generated properties and attempted proofs.

These are useful research directions, but success counts without their attempt and token budgets would omit an important condition. The release is not evidence that every proof can be generated quickly or that every inferred property expresses the developer’s intended behavior.

Budget proof search explicitly

Our analysis: organizations evaluating the update should treat a proof attempt as a scheduled computation with a stopping rule. Record elapsed time, resource consumption, repository state, and whether the resulting artifact passes the selected verifier. An unlimited search can make a model appear more capable while obscuring its usefulness within a delivery deadline.

Property generation deserves a separate review stage. A verified theorem about the wrong behavior does not establish that a program meets its requirements. Keep intended specifications visible to reviewers and track which assumptions were introduced during translation.

Start with a fixed collection of known obligations and compare completed, accepted proofs at the same resource budget. That makes the experiment a decision about practical proof assistance rather than an unqualified leaderboard comparison.