Leanstral / 1.5
How a proof checker turns a model’s attempts into reliable feedback
A language model can write a convincing proof that hides a mistake. A proof assistant such as Lean removes the guesswork: it checks a formal proof step by step against an exact statement and an explicit list of assumptions, and rejects anything that does not follow. Leanstral, released by Mistral AI in March 2026, is an open-weight model trained to write such proofs inside real software projects, using Lean’s feedback as it works. Lean’s verdict, not the model’s confidence, decides whether a proof stands. [1]
Release: . Mistral released the first Leanstral weights on March 16, 2026. Training details from the Leanstral 1.5 announcement and report of July 2 are labeled where they appear.Model: 119B total · 6.5B active (2603 checkpoint)Weight license: Apache 2.0
A checker needs an exact statement
Take the statement “adding zero to a number leaves it unchanged.” Before anything can be checked, the statement has to say what kind of number and what kind of addition, for example natural numbers with ordinary addition. A proof must then show the property for every such number, not just test zero, one and a million.
Now take “adding one always makes a number larger.” That holds for the natural numbers, which have no maximum. It fails for the fixed-width integers computers use, where adding one to the largest value wraps around to the smallest. The English barely changed, but the answer did. A proof assistant checks the formal statement it is given. Making sure that statement matches what a program is meant to do is a separate job.
At the core of Lean is a small program, the kernel, that checks each proof against the statement it claims to prove and the assumptions it may use. Automated tactics help build proofs, but a persuasive explanation is not a proof until the kernel accepts it. This division of labor lets a fallible model propose candidates for a strict checker to accept or reject. [2]
Working inside the feedback loop
The March release of Leanstral targets proof work in Lean 4 projects. It works through Mistral Vibe, Mistral’s coding agent, and the Lean language server, which reports errors and remaining proof goals as the agent edits. The checkpoint, released under Apache 2.0, has 119 billion parameters in total and about 6.5 billion active per token. The mixture-of-experts design is standard; what is distinctive is the training for formal proof work. [3]
Imagine the agent needs a helper lemma before the requested theorem will compile. It searches the project’s library, writes a candidate lemma, reads the goals Lean says remain, and fills in the missing step. Each error message tells it what is still unproved.
The final check also has to confirm that the requested statement was proved as written. Quietly weakening a theorem would produce an easy proof of the wrong thing. Leanstral was evaluated on proof-engineering tasks in whole repositories, not only on isolated competition problems. [1]
The model proposes; the tools show what remains
Rewarding a completed session
Mistral’s July update, Leanstral 1.5, and its report describe three training stages: further pretraining on domain data, supervised training on recorded agent sessions, and reinforcement learning with an algorithm called CISPO. [6] The training environments include repeated attempts at a theorem with compiler feedback, and longer repository tasks with file access and Lean tools. The final check confirms that the statement was not changed and that no disallowed axioms were used. [4]
Think of one training session as a full stint at a workbench: open files, try a lemma, read an error, repair the proof, submit. The report assigns the final outcome’s reward to all the tokens the model generated in that session. Tool outputs and prompts serve as context but are not themselves trained on. This teaches choices that lead to a checked result without separately checking each intermediate sentence.
Long sessions also need memory management. Leanstral 1.5 compacts its context when it grows too long, keeping the original instruction. Its standard evaluation in Vibe uses no special proof-search machinery beyond this compaction. A long session therefore does not mean every earlier token stays in the model’s context. [4]
More attempts, more chances
Because a checker can recognize a valid proof, making several attempts helps. Suppose each attempt succeeds with probability 0.2, independently of the others. The chance that at least one of four succeeds is 1 − 0.8⁴ ≈ 0.59. Real attempts can share the same blind spot, so independence is an assumption, not a fact about the model.
The figure separates total work from elapsed time. Four independent attempts that take 3, 2, 4 and 1 time units need 10 units on one worker. More workers shorten the wait, but the total work stays at 10 units. Real serving adds batching effects, memory limits and tool delays.
Leanstral reports results with several attempts per problem. The figure shows independent attempts, not agents that cooperate on one proof, and it is not a measured Leanstral speed. The report lists cooperative multi-agent proving as future work. [4]
Total work versus elapsed time
What a passed check proves
A Lean file can compile while still containing a placeholder for an unfinished proof, or while relying on an extra axiom, an assumption accepted without proof. Compiling is therefore not enough to count as success. Lean can list the assumptions a theorem depends on, and each task must say which are allowed. In the LeanGym repository tasks, the checker may permit axioms or unfinished pieces that the reference solution itself depends on. A pass means the proof is valid given those permitted assumptions; it does not certify that the whole repository is free of them. [4] [5]
Ask three separate questions of any verified result. Did the proof check? Were its assumptions allowed? Does its formal statement say what was intended? Leanstral’s contribution is a trainable agent, open to inspection, built around this workflow. A model’s confident explanation is no substitute for the checked proof itself.
Simplifications and limits
- Facts about the March checkpoint and training details from the July 1.5 report are labeled separately.
- A checked proof establishes its formal statement under its assumptions; it does not show that the statement matches the English requirement.
- The scheduling figure models independent attempts only, not real serving performance or cooperating agents.
Sources and further reading
Primary papers, model cards, and release posts. Facts describe the versions named here; the interactive calculations are teaching models. Research cutoff: October 3, 2026.
- Mistral: Leanstral releaseMarch 16 public weights, Lean repository tasks, Vibe scaffold and repeated-attempt evaluation.
- Lean reference: Validating ProofsKernel checking, proof terms and the boundary between proof generation and validation.
- Leanstral-2603 model cardApache 2.0, 119B total / 6.5B active parameter specification, inherited sparse architecture and tooling.
- Leanstral technical report (July 2026)Full report read: 1.5 training stages, LeanGym verification, CISPO trajectories, context compaction, ordinary Vibe evaluation and multi-agent future work.
- Lean reference: AxiomsAllowed axioms, unfinished-proof placeholders and assumption auditing.
- Mistral: Leanstral 1.5July 2, 2026 announcement; open weights and report link establish the later update discussed here.