Leanstral: Mistral's Open-Source Lean 4 Proof Agent

Mistral AI released Leanstral on March 16, 2026: an open-source coding agent built for Lean 4, the proof assistant, shipped as Apache 2.0 weights alongside a free API endpoint and an agent mode inside Mistral Vibe. Mistral calls it the first open-source code agent designed for Lean 4. Its design brief applies beyond Lean: code generation has scaled faster than human review, and the time and expertise needed to manually verify machine-generated logic is now the main drag on engineering velocity. Their proposed fix is an agent that carries out the task and formally proves the implementation against a specification, so the human states what they want.

The release includes an architecture, a benchmark with published costs, and two case studies that show the agent doing proof-engineering work.

What Leanstral is

Leanstral is a sparse mixture-of-experts model, 120B total parameters with 6B active (Leanstral-120B-A6B), trained specifically for proof engineering in Lean 4. Lean 4 sits in an unusual spot among formal tools: it is expressive enough for frontier research mathematics (Mistral cites perfectoid spaces) and for software specifications, such as properties of Rust fragments. That range makes a Lean-native agent relevant beyond the theorem-proving community; the same machinery that checks a research proof can check a claim about a program.

Two design choices distinguish it from prior automated proving systems. First, Mistral says most existing systems are wrappers around large generalist models or narrow solvers aimed at single math problems; Leanstral was trained to operate in realistic formal repositories, with their build systems, dependencies, and existing proof libraries. Second, it was trained to work through tooling: it supports arbitrary MCP servers via Vibe and was specifically trained to get maximal performance out of lean-lsp-mcp, the commonly used language-server MCP for Lean. An agent that natively drives the language server sees goals and diagnostics the way a working Lean user does.

The release also promises a tech report on the training approach and a new evaluation suite called FLTEval, meant to move proof-agent evaluation past its long fixation on competition math.

Why Lean makes best-of-N sampling pay off

Formal verification changes the economics of sampling. Mistral calls this "parallel inference with Lean as a perfect verifier."

In ordinary code generation, pass@16 is a mostly academic number. Sample sixteen candidate patches and you have sixteen diffs; unit tests are a partial oracle, so a human still has to pick a winner, and the review cost comes right back. In Lean, the kernel is the oracle. A proof either type-checks against the stated theorem or it does not, and a proof that checks is correct (the remaining risk lives in whether the specification says what you meant). You can run many attempts in parallel, discard failures mechanically, and hand a human only work that has already been verified.

Increasing inference spend raises quality without increasing review work. Leanstral's own numbers make the curve visible: a single pass scores 21.9 on FLTEval for $18; sixteen parallel passes score 31.9 for $290. Every point of that improvement is machine-checked before anyone looks at it. A 6B-active model climbing ten points by spending more compute shows scaling behavior that generalist code agents cannot get because they have no verifier of comparable strength to filter against. Anywhere a hard verifier exists, small specialized models can use cheap parallel sampling and mechanical filtering to compete with much larger models running once.

The FLTEval numbers, and how to read them

FLTEval benchmarks completing all the formal proofs and correctly defining the new mathematical concepts in each pull request to the FLT project, an ongoing large-scale formalization effort. PR-level evaluation matters because real proof engineering is repository work; definitions have to fit an existing library, and proofs have to survive its conventions.

Mistral's published comparison, run with Mistral Vibe as the scaffold and no eval-specific modifications:

Leanstral at pass@2 beats Sonnet by 2.6 points while costing $36 against Sonnet's $549, and at pass@16 it beats Sonnet by 8 points for roughly half Sonnet's cost. Against open-weights peers the efficiency gap is starker: Mistral reports GLM5-744B-A40B and Kimi-K2.5-1T-A32B capping out around 16.6 and 20.1 respectively, while Qwen3.5-397B-A17B needs 4 passes to reach 25.4, a score Leanstral clears at pass@2. Claude Opus 4.6 remains the clear quality leader at 39.6, nearly eight points above Leanstral's best showing, at a cost Mistral pointedly notes is 92 times Leanstral's single-pass run.

The caveats are the usual ones for a vendor benchmark. FLTEval is Mistral's own suite and had not shipped publicly at announcement time, the tech report is still forthcoming, the scaffold is Mistral's own harness, and the competitor numbers include "approximately" hedges. The claims about linear scaling with passes and OSS comparisons deserve third-party replication once the eval suite lands. Lean-as-verifier filtering creates a structural advantage independent of the benchmark.

What the case studies show

The two case studies show process and scores.

The first is a question from the Proof Assistants Stack Exchange: a script that stopped compiling in Lean 4.29.0-rc6, a release recent enough that it postdated Leanstral's training data. The failure was a rw (rewrite) tactic that could no longer match patterns involving a type alias declared as def T2 := List Bool. The agent built test code to reproduce the failing environment, then diagnosed the mechanism: def creates a rigid definition that requires explicit unfolding, which blocked rw from seeing the structure it needed to match. The fix was to swap def for abbrev, which creates a transparent alias that is immediately definitionally equal to the underlying type, letting rw match the pattern (L2 n).length again. That is a subtle definitional-equality issue that eats a working Lean engineer's afternoon, diagnosed by reproduction on a compiler version the model had never seen.

The second case study is cross-assistant migration. Mistral took the Imp language definitions in Rocq from Princeton's course materials and asked Leanstral to convert them to Lean. It produced the full inductive evaluation relation, implemented custom notation for command evaluation, and then, given only Rocq theorem statements with no proofs attached, translated the statements to Lean and proved them, including a correctness spec for a command that increments a variable by two. Porting formalizations between proof assistants is tedious, expertise-gated work where a competent agent makes more projects feasible.

How to run it, and what the free endpoint is for

Access comes in three forms. Inside Mistral Vibe, /leanstall activates the agent, then Shift+Tab cycles the model to Leanstral; vibe --agent lean does the same from the command line. There is a free API endpoint, labs-leanstral-2603, which Mistral says will stay highly accessible for a limited period. Mistral wants realistic feedback and observability data to train the next generation of verified code models. The weights themselves are Apache 2.0, downloadable to run on your own hardware, where 6B active parameters puts self-hosting within reach of a serious workstation.

A self-hosted proof agent with open weights, the open-source Lean toolchain as verifier, and machine-checked output does not depend on anyone's API. If the PR-level methodology holds up under outside scrutiny, FLTEval would provide a useful yardstick for this category, and pass@k against a verifier would become a standard measure for verified-codegen efforts.