Mistral built Leanstral to do something most AI models don’t attempt, write formal mathematical proofs that a compiler can verify as correct. Not “pretty sure this is right” correct. Mechanically, provably, no-exceptions correct.
That’s a narrow use case, and the audience for it is small. What nobody expected was that a model trained on IMO-level math problems and abstract algebra benchmarks would end up running against open-source codebases and finding bugs that testing and fuzzing had both missed. Five of them previously unreported on GitHub.
Table of Contents
What Leanstral actually is
Lean 4 is a proof assistant, a programming language where you don’t just write code, you write mathematical arguments that the system checks for logical correctness. It’s used by researchers to verify things like properties of cryptographic systems, compiler correctness guarantees, and graduate-level mathematics. The barrier to entry is high and the tooling has historically required either deep expertise or a lot of patience.
Leanstral is Mistral’s attempt to lower that barrier. It’s a 119B parameter MoE model with only 6.5B parameters active at inference time, built on the Mistral Small 4 architecture, trained specifically to work inside Lean 4’s environment. It doesn’t just suggest proofs, it submits them, reads the compiler feedback, revises, and keeps going until it either solves the problem or runs out of budget. That means it can work on a single theorem for millions of tokens across dozens of compaction cycles, the same way a human researcher might spend days on a hard proof, except it doesn’t stop for sleep.
Its Apache 2.0 licensed, free API endpoint available, and it runs inside Mistral Vibe with a setup that takes about five minutes.
The part that surprised everyone: it found real bugs
The formal verification angle is interesting to a small audience. The bug discovery is interesting to anyone who writes software.
Mistral built an automated pipeline to test it: Aeneas translates Rust code into Lean 4, Leanstral infers what the code is supposed to do, generates correctness properties, then tries to prove them. If all four attempts at proving a property fail, it flips direction and tries to prove the negation instead. A successful negation proof means the property doesn’t hold, which means the code has a bug.
Across 57 open-source repositories, the pipeline flagged 47 violated properties. Eleven pointed to genuine bugs. Five had never been reported.
One of them was an integer overflow in the sign function of a Rust library used for zigzag decoding. On the maximum possible input value, the expression added one to an unsigned 64-bit integer, wrapping it to zero. In debug mode that crashes. In release mode it silently corrupts data. The kind of edge case that only shows up under a specific input that testing suites rarely think to try and fuzzing can miss entirely. Leanstral caught it automatically.
That’s the result that changes the frame on what this model is. Built for math, useful for software correctness. Those two things turn out to be closer than they look.
Related: Mistral Small 4: The Open Source Model Replacing Three of Mistral’s Own AI Models
The math benchmarks: what the numbers actually mean
miniF2F is a standard formal math benchmark covering problems from algebra, combinatorics, and number theory, ranging from high school competition level up to IMO problems. Leanstral 1.5 hits 100% on both the validation and test sets.
PutnamBench is harder. 672 problems from the Putnam Mathematical Competition, which is the most prestigious undergraduate math competition in North America. Problems that routinely stump PhD students. Leanstral 1.5 solves 587 of them at a token budget of 4 million tokens per problem. The number that matters more than the raw score is the scaling curve: at 50,000 tokens it solves 44 problems. At 200,000 tokens, 244. At 1 million, 493. The performance climbs the entire way without plateauing, which means the model is genuinely using additional compute to reason deeper.
FATE-H and FATE-X cover graduate and PhD-level abstract algebra, group theory, ring theory, module theory. Leanstral 1.5 sets a new state of the art on both at 87% and 34% respectively.
The number that puts all of this in context is the cost. Solving a PutnamBench problem with Leanstral runs around $4. The next strongest competitor, Seed-Prover at its high setting, costs an estimated $300 or more per problem and requires 10 H20-GPU-days of compute. That’s not a small gap. It’s the difference between something a researcher can run routinely and something that requires a grant.
Five Minutes to Set Up, Then Just Start Proving
Mistral Vibe handles the agent layer. Install it, run /leanstall inside it, and Leanstral 1.5 is ready. The free API endpoint means no self-hosting a 119B model just to try it. For teams who want local deployment, vLLM support is there with standard serving configuration.
For anyone already using Lean 4, the lean-lsp-mcp integration is worth adding, it gives the model real-time access to goal states, type information, and compiler errors as it works, which is what enables the long-horizon proof sessions.
What Happens When You Run This Against 5,700 Repositories
Five unreported bugs across 57 repositories isn’t a large sample. But it’s a large enough result to ask the obvious follow-up question: what does that number look like at ten times the scale?
Formal verification has always been confined to teams with the budget, expertise, and patience to make it work. The cost argument alone kept most codebases out of reach. At $4 per problem versus $300 for the nearest alternative, that argument is getting harder to make. A model built to prove graduate-level mathematics, running automatically against Rust code and catching integer overflows that fuzzing missed, is either a curiosity or the beginning of something that shows up in standard CI pipelines. The 57-repository sample doesn’t answer that. But it makes the question worth asking seriously.
