Leanstral 1.5

Leanstral 1.5 is an open-weight model from Mistral AI for formal proof engineering in Lean 4. It is designed to operate as a coding agent that edits Lean projects, reads compiler and language-server feedback, and iterates until a proof or definition passes a verifier. Mistral made the hosted Labs endpoint available on June 30, 2026 and publicly launched the model, weights, and technical report on July 2.^[1][5][6]

The model is an update to the original Leanstral released in March 2026. It belongs to the Mistral Small 4 family and retains a sparse mixture-of-experts architecture with 119 billion total parameters and 6.5 billion activated for each token.^[2][3] Leanstral 1.5 is not itself a proof checker. Its output becomes meaningful only when Lean and an appropriate verifier accept a proof against the intended formal specification.

Release and model specifications

Mistral's materials record two dates for the release. The API changelog lists labs-leanstral-1-5 on June 30, while the public launch article is dated July 2.^[1][6] The earlier labs-leanstral-2603 endpoint was retired on June 30 and replaced by version 1.5.^[13]

Scroll sideways for more →

Mistral's launch post and report round the active count to 6B, while the model card gives 6.5B.^[1][2][3] The public configuration also discloses 36 model layers, a hidden dimension of 4,096, one shared expert, and FP8 E4M3 weight quantization. The model card lists image input, but the Lean technical report does not present a vision evaluation.^[3]

The active-parameter count describes computation for one token, not the amount of model data that must be stored. The official Hugging Face repository is about 121 GB and divides the checkpoint across seven consolidated SafeTensors shards.^[4] A local host still needs the expert weights plus runtime and key-value-cache memory.

Training

The technical report describes three training stages. Mid-training starts from a Mistral Small 4 checkpoint and uses 6.5 billion deduplicated Lean-specific tokens, along with general coding-agent data and other instruction-following and alignment sources. The Lean data includes attempts at individual theorems and traces from work on realistic repository issues.^[2]

During supervised fine-tuning, Lean coding-agent traces make up 50% of trainable tokens. Mistral filtered the mixture for correctness, formatting, and style. It also filtered behaviors that are harmful in long proof tasks, such as declaring success without compiling, refusing difficult but feasible work, and inventing repository constraints.^[2]

The final stage uses reinforcement learning with verifiable Lean feedback. Its task mixture is 50% LeanGym pull-request data, 20% LeanGym single-theorem data, and 30% multiturn prove-or-disprove data. Pull-request tasks come from permissively licensed Lean repositories: the pipeline removes selected proof or definition bodies, gives the agent the surrounding repository, and rewards reconstruction that passes verification.^[2]

The optimization method is CISPO, a truncated importance-weighted policy-gradient objective. In the multiturn environment, the model submits a proof or disproof, receives compiler feedback, and tries again. LeanGym gives the agent a filesystem, bash, and Lean language-server tools. The final repository state is checked with Mistral's fork of SafeVerify.^[2][9]

The report does not enumerate the complete training corpus, all general coding and alignment sources, every source repository, or training compute. It also does not publish the full training data or end-to-end training pipeline. The release is therefore best described as Apache-licensed open weights with public evaluation and verifier tools, rather than a fully reproducible training release.

Agent operation and long contexts

Leanstral 1.5 runs in Mistral Vibe, a general coding-agent harness. It can inspect goals and errors through Lean LSP, edit multiple files, invoke shell commands, build helper lemmas, and continue after its working context is compacted.^[2][3] This differs from a specialized prover that builds a separate search tree or orchestrates a fixed collection of proof tactics.

The advertised context window is 256,000 tokens, but Mistral recommends limiting ordinary requests to 200,000.^[3][5] Reported evaluation trajectories can be much larger because Vibe summarizes previous work and starts another window while preserving the original task. For PutnamBench, the largest setting allowed four million accumulated tokens with automatic compaction every 200,000 tokens. That is a multi-window agent budget, not a four-million-token context window.^[2]

Evaluation

Mistral evaluated the model through Vibe and its modified SafeVerify. The results below are vendor-reported. pass@k measures whether at least one of up to k attempts succeeds, so pass@8 is not equivalent to one response being correct.^[2]

Scroll sideways for more →

The launch post says Leanstral 1.5 saturates miniF2F. The report gives a more precise account: its initial pass@4 test result was 242 of 244, and the last two problems were solved only through extra attempts, one after one additional pass and the other after 37.^[1][2]

PutnamBench contains 672 Lean formalizations of undergraduate competition problems.^[10] Leanstral's score rose from 44 solved with a 50,000-token trajectory budget to 587 at four million tokens. The model was below Aleph Prover's 668 and a natural-language-guided Goedel-Architect result of 597 in Mistral's comparison table. The official leaderboard cautions that systems use different guidance and compute budgets, which limits simple rankings.^[2][10]

FLTEval is Mistral's repository-level benchmark built from pull requests to the Lean formalization of Fermat's Last Theorem. The technical report describes 169 tasks. Leanstral 1.5 scored 28.9% at pass@1, 34.6% at pass@2, 38.9% at pass@4, and 43.2% at pass@8. The predecessor scored 21.9%, 26.3%, 29.3%, and 31.0% at the same settings.^[2]

Mistral released a Docker-only FLTEval harness that applies submitted diffs and checks them with Lean and SafeVerify. It includes a prepared 162-instance sample, sample submissions, and evaluation output, but it does not run an agent or generate trajectories.^[8] Reproducing the reported number still requires a model-serving setup, the generation scaffold, substantial inference, and alignment with the report's task set.

No independent reproduction of the complete Leanstral 1.5 benchmark suite was located as of July 24, 2026. An independent document audit likewise treated the scores, cost comparisons, and bug findings as unreplicated Mistral claims.^[12] The cited technical report is vendor-authored and was not identified as peer-reviewed.

Code-verification case studies

One case study asked Leanstral to prove properties of a specific AVL-tree implementation. The agent generated proofs that the tree remained balanced and that insertion and deletion took logarithmic time. The run lasted more than eight hours, produced over 2.7 million output tokens, and required 22 context compactions.^[2] This demonstrates long-horizon persistence, but also shows the time and compute hidden by a final accepted proof.

A second experiment used Aeneas to translate Rust repositories into Lean. Leanstral inferred intended properties, tried four times to prove each property, then tried four times to prove its negation. Across 57 translated repositories, the pipeline flagged 47 violated properties. Review found 11 flags that represented real bugs, corresponding to five unique issues that Mistral said had not previously been reported.^[1][2]

Most flags were not software bugs. They resulted from specifications that were too strong, malformed, or included states unreachable through the public interface.^[2] The experiment therefore illustrates both sides of autoformalization: Lean can rigorously verify a proposition, but a model-generated proposition may fail to express the programmer's actual intent.

Access and hardware

The model weights are available from Hugging Face under Apache 2.0.^[3] At the research cutoff, Mistral also listed the hosted endpoint at no charge after a user opted into Labs and created an API key. The recommended Vibe workflow is to run /leanstall and then vibe --agent lean.^[3][5]

Mistral's local-serving instructions use vLLM 0.24.0 or newer, mistral_common 1.11.5 or newer, a 200,000-token model length, the FLASH_ATTN_MLA backend, and four-way tensor parallelism.^[3] They do not name a minimum GPU model or memory capacity. The 121 GB checkpoint size means the official weights alone do not fit on an ordinary single 24 GB accelerator; long-context cache and runtime overhead add further memory demand.^[4]

The hosted model is a Labs release. Mistral says Labs models are experimental, can change quickly, may be removed with two weeks' notice, and are not recommended for production.^[7] The changelog scheduled this endpoint for retirement on September 30, 2026.^[6] Downloaded weights are not tied to that hosted retirement date.

Verification, safety, and limitations

SafeVerify adds checks beyond simply asking whether a file compiles. It replays declarations with Lean's kernel, checks that required names and types match the trusted target, restricts accepted axioms, and rejects partial or unsafe definitions.^[9] Mistral's training verifier also disallows native_decide, a mechanism with known consistency concerns in this setting.^[2]

These checks have boundaries. SafeVerify's own documentation says it does not automatically catch every use of implemented_by, extern, or noncomputable, and does not replay imported modules unless configured for a fresh check.^[9] Official Lean documentation similarly explains that a proof check is meaningful only when the theorem statement is correct and potentially malicious code is built in an appropriate sandbox.^[11]

Formal acceptance does not prove that a specification captures the real-world requirement, that translated source code preserves all behavior, or that an agent's unrelated file changes are safe. Leanstral can run shell commands and modify a repository, and Mistral explicitly warns users to be careful with Vibe's auto-approval mode.^[3] Generated changes still require review, sandboxing, version control, and an independently trusted verification configuration.

The report also records residual model limitations. Earlier checkpoints sometimes announced success without compilation, refused hard tasks, or drifted after repeated compaction. Training filters and prompt preservation were designed to reduce those failures, not prove their elimination. On research-level ArXivLean tasks, the final model solved 17.1% and sometimes stopped after incorrectly deciding that dependencies were missing.^[2]

Leanstral 1.5's strongest evidence is therefore narrow: it can generate many machine-checkable Lean artifacts when given repeated attempts, large token budgets, tool access, and a controlled verifier. It does not establish general mathematical reliability, automatic software correctness, or safe autonomous repository operation.

References

1. Mistral AI. Leanstral 1.5: Proof Abundance for All. July 2, 2026. ↩
2. Mistral AI. Leanstral. Technical report, July 2, 2026. ↩
3. Mistral AI. Leanstral 1.5 119B A6B model card. Hugging Face. ↩
4. Mistral AI. Leanstral 1.5 repository files. Hugging Face. ↩
5. Mistral AI. Leanstral 1.5 API model card. Mistral Docs. ↩
6. Mistral AI. Changelog. Mistral Docs. ↩
7. Mistral AI. Labs model policy. Mistral Docs. ↩
8. Mistral AI. FLTEval. GitHub. ↩
9. Mistral AI. LeanstralSafeVerify. GitHub. ↩
10. Tsoukalas, G. et al. PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition. NeurIPS 2024 Datasets and Benchmarks. ↩
11. Lean project. Validating a Lean Proof. Lean Language Reference. ↩
12. Future Stack Reviews. Leanstral 1.5: Free Model, Not the Verification System. July 2026. ↩
13. Mistral AI. Leanstral v26.03 model card. Mistral Docs. ↩