- Model Release: Mistral AI has released Leanstral 1.5 as a free Apache-2.0 model for machine-checkable proof work.
- Proof Workflow: Its workflow submits proofs, receives compiler feedback, and can use developer-tool actions while working through verification tasks.
- Mistral’s Claims: Mistral claims 587 of 672 PutnamBench problems, about $4 per problem, and 5 previously unreported GitHub bugs.
- Prover Race: Rival theorem-proving projects including Seed-Prover, AlphaProof, Goedel-Architect, Aleph Prover, and OpenATP keep the category crowded.
Mistral AI has released Leanstral 1.5 as a free Apache-2.0 model for Lean 4 verification. Lean 4 is a proof-assistant and programming environment for machine-checkable proofs, and proof engineering means building those proofs and fixing them when the checker fails.
Lean has become a favored tool for formal mathematics and verified software because it forces every step of a proof to pass a strict checker, leaving little room for ambiguous reasoning. But that precision also makes Lean proofs labor-intensive: users often spend significant time translating ideas into formal syntax, resolving missing lemmas, and fixing compiler errors. AI prover systems such as Leanstral aim to reduce that burden by acting more like coding agents for proofs, proposing Lean code, reading feedback from the checker, and revising their work until the proof succeeds.
How Leanstral 1.5 Turns Proof Work Into a Developer Tool
Model scale starts with 119 billion total parameters and 6 billion active parameters. Its labs-leanstral-1-5 endpoint carries 119B total parameters, 6.5B active parameters per token, and a 256k context window.
It uses a mixture-of-experts architecture with 128 experts and 4 active experts per token, while local deployments should stay within up to 200k tokens even though the model supports the larger context length.
In the company figures, Leanstral 1.5 reaches 100% on miniF2F, 587 of 672 PutnamBench problems, 87% on FATE-H, and 34% on FATE-X. Cost figures put Leanstral at about $4 per problem on PutnamBench, compared with $300 or more for Seed-Prover 1.5 high.
Leanstral 1.5 uses a multiturn training environment where the model submits Lean proofs, receives compiler feedback, and refines attempts until it solves a problem or exhausts its budget.
Leanstral can edit files, run shell commands, and use the Lean language server, an editor-style service that returns proof or code feedback while the model works.
An evaluation on 57 repositories flagged 47 violated properties, 11 genuine bugs, and 5 previously unreported GitHub bugs.
One example involved AVL-tree insertion and deletion time-complexity guarantees after a proof run of more than 2.7 million tokens and 22 compactions.
A Crowded Race for Lean-Based Provers
Leanstral enters an active Lean prover category rather than an empty field. DeepSeek-Prover-V2-671B supplied another scale marker as a 671B-parameter Lean 4 theorem-proving model made available on Hugging Face.
ByteDance Seed rolled out Seed Prover 1.5 in December 2025 as a specialized formal mathematical reasoning model, and Seed-Prover 1.5 uses agentic reinforcement learning with test-time scaling.
Google DeepMind introduced AlphaProof and AlphaGeometry 2 in July 2024, when the systems solved IMO problems at silver-medal level. AlphaProof Nexus later added Lean-checked Erdős and OEIS results, making it a nearer comparator for machine-verified proof workflows. Mathematician Prof Sir Timothy Gowers later treated one AlphaProof construction as a non-obvious machine-reasoning result.
Recent Lean-verified mathematical proofs explain why workflow matters alongside benchmark tables. Goedel-Architect framework is a Lean 4 theorem-proving system built around blueprint generation and refinement.
Aleph Prover 0.2.3 reached PyPI on May 19 as a Lean proof-request tool. OpenATP interface offers an open interface for Lean-focused provers, lists Leanstral among available integrations, and includes benchmark utilities for PutnamBench, FATE-H, FATE-M, and FATE-X.
Access, Cost Claims, and What to Watch
Developers can test the access path directly. Leanstral 1.5 is available on Hugging Face and through the free leanstral-1-5 API endpoint. A labs model optimized for automated theorem proving also targets autoformalization.
Apache-2.0 licensing makes local inspection and downstream experimentation more practical than a closed API-only release. Developers can compare the PutnamBench cost estimate, repository bug count, and local deployment guidance against their own Lean projects. Repository evaluation surfaced 5 previously unreported GitHub bugs, so the concrete next gate is independent reproduction on real Lean codebases.
