Mistral releases Leanstral for repository-scale proof engineering

Mistral released Leanstral on March 16 as a coding agent specialized for Lean 4 proof engineering. The announcement makes the weights available under Apache 2.0 and describes integration with Mistral Vibe. Its intended work includes navigating formal repositories, constructing proofs, and adapting definitions, rather than only answering isolated mathematics questions.

Repository work becomes the target

Mistral presented FLTEval, an evaluation based on changes in a Fermat’s Last Theorem repository, alongside its release. The company reports results under different inference budgets and compares them with other agents. Those figures describe its selected tasks and setup; this brief does not independently reproduce the results.

The distinctive engineering proposition is an agent working with a proof checker. Generated artifacts can be checked against a formal statement instead of being accepted because the accompanying explanation sounds plausible.

Review the statement as well as the proof

Our analysis: a successful proof still leaves an important human decision—whether the formal statement expresses the requirement the team actually intended. An agent that strengthens an assumption, weakens a conclusion, or changes a definition may make a proof easier while changing its usefulness.

A pilot should therefore separate editable implementation files from protected specifications. Review changes to assumptions, dependencies, and theorem statements explicitly. Keep the compiler version and library revision fixed while comparing runs, and record both failed attempts and completed artifacts.

For teams already using formal methods, the practical next step is a small backlog of unfinished proofs with known acceptance criteria. Measure how much expert review remains after verification, not simply how many files the agent edits or how convincing its explanation appears.