---
title: "Mistral's Leanstral 1.5 Solves 587 Putnam Problems at $4 Each"
subtitle: "Mistral's Leanstral 1.5 solves 587/672 Putnam problems at ~$4 each, finds 5 unreported open-source bugs, and scales smoothly to 4M tokens"
url: "https://alphasignal.ai/news/mistral-s-leanstral-1-5-solves-587-putnam-problems-at-4-each"
author: "AlphaSignal Newsroom"
author_url: "https://alphasignal.ai/editorial-team"
company: "Mistral AI"
company_url: "https://alphasignal.ai/company/mistralai"
published: "2026-07-04T07:50:31.414Z"
updated: "2026-07-04T07:52:31.161Z"
type: "Model"
topics:
  - "Development"
  - "Open Source"
subtopics:
  - "Code Agents"
upvotes: 1473
source_url: "https://huggingface.co/mistralai/Leanstral-1.5-119B-A6B"
comments: 0
truncated: true
---

# Mistral's Leanstral 1.5 Solves 587 Putnam Problems at $4 Each

> Mistral's Leanstral 1.5 solves 587/672 Putnam problems at ~$4 each, finds 5 unreported open-source bugs, and scales smoothly to 4M tokens

[Leanstral 1.5](https://mistral.ai/news/leanstral-1-5/) is Mistral's latest formal-reasoning model, built specifically for [Lean 4](https://github.com/leanprover/lean4), the proof assistant used to mechanically verify everything from graduate-level algebra to software correctness. The model is free, Apache-2.0 licensed, and available right now via a free API endpoint and on Hugging Face. If you have never touched formal verification before, this is the cheapest on-ramp that has ever existed.

## What Lean 4 actually is, and why it's hard

In mathematical proofs and software verification, small mistakes can lead to major problems, so formal proof support systems like Lean 4 are used to demonstrate correctness in a way that computers can verify. The catch is that expressions that humans commonly use, such as "obviously true" or "can be proven in the same way," are not understood by computers. Every step needs to be translated into a form Lean 4 can check, which is a time-consuming process, and why dedicated AI models are needed to assist.

The field has been heating up. Lean 4 has been quietly turning into the venue where frontier labs argue about reasoning, with models from DeepSeek, ByteDance (Seed-Prover), and now Mistral all competing on the same benchmarks. The difference with Leanstral 1.5 is the cost-to-performance ratio.

## The numbers that matter

Leanstral 1.5 saturates miniF2F completely, reaching 100% on both the validation and test sets. miniF2F covers problems from elementary math up to IMO-level challenges. Beyond that, the headline result is PutnamBench: Pass@8 on PutnamBench climbs from 44 problems solved at 50k tokens to 244 at 200k, 493 at 1M, and 587 at 4M.

Here is how Leanstral 1.5 stacks up across benchmarks:

| Benchmark              | Leanstral 1.5 | Notes                |
| ---------------------- | ------------- | -------------------- |
| miniF2F (val + test)   | 100%          | Fully saturated      |
| PutnamBench            | 587 / 672     | \~$4 per problem     |
| FATE-H (grad. algebra) | 87%           | New state-of-the-art |
| FATE-X (PhD algebra)   | 34%           | New state-of-the-art |
| FLTEval pass@1         | 28.9          | Up from 21.9         |
| FLTEval pass@8         |               |                      |

_Preview only. Full text requires an AlphaSignal Pro account._

## Sources

- [Leanstral 1.5: Proof Abundance for All – Mistral AI](https://mistral.ai/news/leanstral-1-5/)
- [mistralai/Leanstral-1.5-119B-A6B – Hugging Face](https://huggingface.co/mistralai/Leanstral-1.5-119B-A6B)
- [Mistral AI Releases Leanstral 1.5 – MarkTechPost](https://www.marktechpost.com/2026/07/03/mistral-ai-releases-leanstral-1-5-an-apache-2-0-lean-4-code-agent-model-solving-587-of-672-putnambench-problems/)
- [Mistral ships Leanstral 1.5 for Lean 4 proof work, free in Labs – AI Weekly](https://aiweekly.co/alerts/mistral-ships-leanstral-15-for-lean-4-proof-work-free-in-labs)
- [Mistral releases Leanstral 1.5 for automated theorem proving – GIGAZINE](https://gigazine.net/gsc_news/en/20260701-mistral-leanstral-1-5/)