AI Researcher @ Mistral AI | Formally IBM Research | Former Mathematician/Logician/Data scientist | Building AI for math and reasoning
- Tweets 1,012
- Following 263
- Followers 950
- Likes 3,833
Pinned Tweet
So excited to introduce Leanstral 1.5, an open source @leanprover code agent model which is SoTA on FATE-H/X, 587 on PutnamBench, and solves all of MiniF2F with only 6B active parameters! It is free to use, so give it a try!
mistral.ai/news/leanstral-1-…
Leanstral 1.5 is here. SoTA on FATE-H/X, 587 on PutnamBench, saturating miniF2F, all with an Apache-2 6B active params model. We are having fun verifying code properties and catching bugs in Rust repos!
Tech report covering training environment and evaluations: github.com/mistralai/Leanstr…
We also open-source LeanstralSafeVerify and FLTEval.
1
1
14
3,023
For those keeping track of open problems (or applying AI to them), I just found this list of open logic problems by Patrick Lutz including some I really like such as KL Randomness vs ML randomness (which I think might be ready for AI). openlogicproblems.com
4
4
42
3,369
The First Sylow Theorem was the first significant theorem I ever formalized (in HOL light). Fast forward 20 years and a 6B active param model can do this (and much more!) automatically. The systematic formalization of most of math has never been closer!
Ran Leanstral 1.5 from @MistralAI on the First Sylow Theorem by Peter Ludwig Mejdell Sylow. Not the hardest theorem the model claims to handle, but a strong test of agentic proof engineering .
The constraint was simple: everything had to be derived from Cauchy's theorem and induction, with lean-lsp-mcp providing live compiler diagnostics, goal states and Loogle throughout the run.
The proof took 28 minutes and 380K tokens. Compaction held up well.
The screenshot is a compressed 3 step view for readability . the actual run went through 10 debugging phases before converging.
Very impressive model from the Mistral AI team.
1
3
31
3,537
Jason Rute retweeted
Today, we are releasing Le Chaton L∃∀N, aka Leanstral 1.5.
It achieves SOTA performance on graduate algebra benchmarks FATE-H and FATE-X and improves Pareto Frontier on PutnamBench, solving 587/672 problems with a x10 cheaper budget.
🧵
77
154
1,480
338,615
Jason Rute retweeted
Leanstral by @MistralAI is now available in OpenProver!
openprover theorem.md --model=leanstral
I'm releasing OpenProver v1.0.0!
It's 1) an open-source automated theorem prover inspired by DeepMind's Aletheia (@tonylfeng @gjb_ai @lmthang), and 2) a "Claude Code for mathematicians", allowing interactive proof search in English and formalization in Lean.
1
17
71
6,604
Jason Rute retweeted
Interested in Lean and near 🇫🇷 Paris?
The inaugural Paris Lean Meetup is happening April 24 at 7:00 PM, hosted by Mistral AI.
Two talks: Leonardo de Moura of Lean FRO, and the Mistral team introducing Leanstral, their open-source code agent for Lean 4.
Pizza and informal discussion afterward.
🔗 Registration details here: meetup.com/lean-paris/events…
4
16
159
13,071
Someone built an app for Econ Autoformalization in Lean using #Leanstral. Looking forward to seeing more tools like these!
I would love some expert guidance on how to get the most out of leanstral. Here is the API’s repo and a little demo im working on with lovable. Happy to chat outside the thread!
leanecon-demo.lovable.app/
github.com/Bonorinoa/lean_ec…
2
3
15
1,635
Jason Rute retweeted
So far, it has been absolutely great to work with. Thank you to the entire #Leanstral team this is exactly the kind of project we need more people working on.
1
1
204
Thanks, @Leonard41111588 ! And thanks for making such an awesome language! We really hope #Leanstral is a benefit to the Lean community, and we are actively working on making it even better!
Congratulations to the Mistral team! Great to see a dedicated open-source Lean 4 coding agent. The Lean community is growing fast, and tools like Leanstral will help more people get productive with Lean quickly. Looking forward to seeing how it evolves.
1
2
20
1,561
Announcing our fully open source code agent to support development in @leanprover. This has been a labor of love by our team at @MistralAI and we look forward to seeing what the #LeanProver community does with it!
1
27
160
10,695
Use for free in Mistral-Vibe:
$ uv tool install mistral-vibe --upgrade
$ vibe /leanstall
Then shift+tab to lean mode
1
18
667
More information here including examples: mistral.ai/news/leanstral
1
21
529
Last time I saw someone drop a Lean “proof” of a Millennium Problem it didn’t remotely compile. I hope in this case the error is at least interesting. :)
Update: David claims to have a Lean proof of Navier-stokes, which he is publishing tonight.
I have accepted a $10,000 bet that he's mistaken.
9
2
144
19,558
Jason Rute retweeted
Thrilled to announce @MistralAI's new formal math team following our $2B funding round.
AI for formal math researchers wanted. We offer:
- Work on creating the state-of-the-art prover, autoformalizer, and automatic proof agent all in one model
- World class team (with @JasonRute @sorgfresser @Icannos myself and support from @GuillaumeLample)
- A huge bias for action
- Hundreds of GPUs per capita with Mistral’s bleeding edge reinforcement learning pipeline (responsible for Magistral and Magistral 1.2)
- Open research with publications
- Industry-leading salary
- Offices in Paris, London, and Palo Alto
To apply: Experiences in AI required. Send your CV and best work on AI and/or formal math to aj@mistral.ai, with <formal> in the email title.
14
47
518
80,133
For those using @leanprover AI models to “compete” in #imo2025 (@ProjectNumina , @KaiyuYang4), what Lean formalizations will you use? (A) autoformalized statements, (B) manually formalized statements, (C) Joseph Meyer’s IMOLean formalizations (github.com/jsm28/IMOLean)?
2
4
20
2,106
At #JMM2025 last week, a mathematician told me he used ChatGPT (forgot which version) to get a major insight into solving his math problem. But, he is reluctant to share publicly (e.g. in his paper) that this happened since it could make him look less bright. I find this sad. 🧵
4
3
67
8,762
If we aren’t willing to talk about when tools are helpful, it will lead to an asymmetry where those in the know will use hidden methods that they keep secret out of either embarrassment or competition. IMHO, this isn’t in the spirit of mathematics research.
2
23
1,359