10 ms·

Leanstral 1.5

310 points by vetronauta 3mo ago

__natty__ 3mo ago
Discussion about Leanstral 1: https://news.ycombinator.com/item?id=47404796 https://news.ycombinator.com/item?id=47404796
doctorpangloss 3mo ago
Real talk, does anyone use anything from Mistral because it performs the best, by whatever secular metric of your choosing? Or is it only used "because EU"? Just focus on answering the question. I wonder if anyone has observed it perform better on any objective metric in any rigorous setting.
- trentor 3mo ago
  I like the models for creative writing. They have a distinct voice that is different from the other llms.
  - SwellJoe 3mo ago
    I made a game (https://prose-or-con.com https://prose-or-con.com) where you pick whether writing is AI or human. Mistral is a bonkers weird writer. So weird I fell for it a couple of times because I thought, "No way a model writes this weird." Not, like, incorrect grammar or spelling or anything, just...off-kilter. Kinda sassy.
    - vlian2088 3mo ago
      needs a leaderboard of models most often mistaken for humans.
      - SwellJoe 3mo ago
        Yes, it's on the todo list, but I need more data. Only a half dozen people have played it and submitted a score. I'm storing the hashes of passages people got right and wrong so I can make exactly that chart at some point. I think both "the most human-like AI" and "the most AI-like human" are both interesting pieces of data, but I don't know either yet.
        vlian2088 3mo ago
        try posting it on r/localllama and r/sillytavernai
- troyvit 3mo ago
  We are not Mistral's target audience. For instance I don't know if Leanstral performs the best as a "formal proof engineering model optimised for automated theorem proving and autoformalization" because I don't even know wth that is or who else does it. Mistral themselves focus more on b2b; financial services, manufacturing, stuff like that, and they get some big clients that way. Despite not being their target, I started using them because they have many open models. I continue using them because, yeah EU, but also because the community is great and the tool makes me think more than Claude does. Last, I stick with them because they are one of the few AI companies that are up-front about their environmental impact and are actually trying to minimize it while still providing a decent product.
  - computerex 3mo ago
    It's for mathematics. There is this programming language: https://lean-lang.org/ https://lean-lang.org/ If you can express a solution in Lean you can formally prove or disprove it. Formal verification is making a debut in traditional engineering toolkits.
- data-ottawa 3mo ago
  Mistral medium is considerably better at writing than Opus. I’ve also found it very good at pulling info from pdfs. Even a complicated festival with multiple venues and timetables.
  - tjwebbnorfolk 3mo ago
    Writing what? I found it worse than gemma4 at coding even though it's 4x the parameter size
- Adrig 3mo ago
  A few months ago, I had some data cleaning to do; their small model was surprisingly efficient and got the job done for 0.2x what I expected to run (Anthropic Sonnet / Haiku). Their TTS / STT is also roughly at the frontier, at least for French. But I admit I only consider them because they're from France. Haven't seen a dimension where they're competitive for general users
- evilmonkey19 3mo ago
  I use it because EU and API pricing is decent to me. And support is awesome also. They reply the same day or at most the next day, and they follow the ticket great. It isn't that bad, but neither the best.
  - jatora 3mo ago
    Why do you need support so often?
- adev_ 3mo ago
  > Mistral because it performs the best, by whatever secular metric of your choosing? I am. I use them primarily through their vibe CLI. Reason is simple: They are cheaper (by almost one order of magnitude compared to Claude) and still do the job pretty well. For small programming tasks, quick prototyping, refactoring or anything verbose and not requiring a context too large: I first go to Mistral and then eventually to Claude if I'm unsatisfied. I also found out some of their models to be more responsive than OpenAI ones (which is not so surprising considering the size). My tasks are mainly C++ and Python programming. People in other languages might not share my enthusiasm.
  - jatora 3mo ago
    Your reason can't be cost because there are superior models that are cheaper than Mistral models, for coding. So i re-ask the question
    - adev_ 3mo ago
      > Your reason can't be cost because there are superior models that are cheaper than Mistral models Nope. This is not my experience. Public pricing in token/$ is only part of the equation. Mistral tooling to consume significantly less tokens-per-given-task than the Anthropic ones. My bills currently reflects that.
      - tjwebbnorfolk 3mo ago
        I think other commenter is talking about smaller/cheaper models like Qwen that outperform mistral on just about every metric
        adev_ 3mo ago
        I played with Qwen few months ago, I do prefer Mistral vibe for everyday usage (significantly faster if not self hosted).
      - greenavocado 3mo ago
- hakunin 3mo ago
  I use it because it’s a simple, convenient and cheap OCR api. Specifically via my ringbinder[1] tool. [1]: https://github.com/maxim/ringbinder https://github.com/maxim/ringbinder
- Confiks 3mo ago
  For writing and languange learning it's very decent, especially Mistral Large. The pricing is very good too. I really like the consistently low time to first token and good token per second. Claude, especially in the past, would be very inconsistent, often with outages. Mistral mostly just always works and is very fast. Technical questions are unfortunately hit or miss. I'm lately pretty much always using a system prompt that emphasizes short answers [1], and Opus regularly one-shots it while Mistral needs a follow up. I use big-AGI as a model router [2] (dumb name, great software), which makes switching midway very easy though. For coding I'm still using Claude Code mostly out of inertia (although I really want to move to an OSS harness) and the one time I tried their `vibe` tool months ago it was a bit rough. Mistral TTS with diarization is also great and cheap. That's the only thing for which I use their web UI. [1] Give a short but helpful answer to the question the user asks. When helping with a computer-related task, unless the user asks, don't give any installation or setup instructions, but just get straight to the point. When the user asks a follow up question, give a more complete and longer answer while still not overexplaining. When the user prefaces the question with "short mode off" in any question, give a full and well considered reply. [2] https://github.com/enricoros/big-AGI https://github.com/enricoros/big-AGI
  - Skinney 3mo ago
    vibe has improved _a lot_ during the past few months, fyi. The new Mistral Medium 3.5 is also a big improvement over devstral-2
  - BartjeD 3mo ago
    Mistral doesn't have caching on batches. For me that meant they are 10x more expensive than Google. I think its dumb. Their support is hidden away in a chat bubble at the bottom. But they do respond promptly. Its decent, but after switching to Google i wouldn't go back
- ashenke 3mo ago
  I use their Voxtral Mini STT audio model to automatically transcribe my podcasts into markdown. Out of all the STT models I've tried, it's both the best performing and one of the cheapest! It's really accurate, feeding the episode notes and the podcast description ensures all names are properly spelled, and speaker diarization works really great. (I just do a Gemini flash pass at the end to identify the speakers, so it shows the host name instead of "Speaker 1")
- refulgentis 3mo ago
  OCR is off the charts good on every metric you can think of. LLMs are a near-afterthought at this point if you don’t have data residency requirements. I love them and they’re slightly underrated, their models are consistently well-trained, open, but as you note, behind. There is no metric that will say they’re ahead in anything.
  - cavenditti 3mo ago
    This. Best OCR provider by measure and it’s been for years
    - urbsgpw 3mo ago
      Hmm, not sure I'd agree. I really like google's offering there (they suck at coding agents but their OCR is good value for money - well up till the latest flash model which has got wicked expensive). See also https://www.ocrarena.ai/leaderboard https://www.ocrarena.ai/leaderboard I know these leaderboards are iffy, but at least my experience has been somewhat similar.
      - refulgentis 3mo ago
        Thank you for sharing this, I’ve had some disquiet around the release blogs…something felt cherry-picked and I didn’t know there was a 3rd party source for evals, that settles it easily - like you said they can be iffy but there’s a clear enough gap and large set of models for me to let go of the idea it’s the best by some margin.
- suprjami 3mo ago
  I still prefer Mistral Nemo 12B for text summarisation tasks. It has a nice style. The Mistral Small 24B is also decent. I have a YouTube transcript summariser which I like these for. However these days I usually have Qwen 3.6 27B already loaded so I mostly just use that instead.
- bee_rider 3mo ago
  I liked that their website didn’t ask for my phone number, IIRC.
- Hamuko 3mo ago
  >Just focus on answering the question. Are you trying to instruct me like an LLM?
- psalaun 3mo ago
  I use it as my workhorse for coding and general chat questions, because it's good enough 80% of the time, and indeed it's french/european (with heavy US capital tho...). We complain too much about not having enough major competitors in the IT space, to not support a burgeoning one even if it's less powerful than SOTA labs
  - barrenko 3mo ago
    Well, if you're a taxpayer in EU you're already supporting it implicitly.
- istinetz 3mo ago
  For a defense project we're working on, we basically have a hard requirement to use european cloud provider + european llm We cannot use open source LLMs on-prem, I asked. So that's basically a hard requirement to use mistral, even though Chinese models are strictly better on every dimension.
  - angry_octet 3mo ago
    Is there a rationale behind why not on prem? Boogeyman fears about LLMs? No hardware? Or do you mean, no Chinese LLMs?
- anonyfox 3mo ago
  just used mistral for a database/scraping creation tool and ended at <10k€ in token costs (via openrouter), beating gpt5.4-mini in output quality and speed and costs after actual testing A/B fairly. so its a super scoped task to be performed hundreds of thousands of time for some automation and mistral just did it better across all dimensions that gpt-5.4-mini. of course thats not a headline in terms of frontier model competitiveness, but for "the boring parts" it just was flat out better than anything else consistently. bonus points it handles mixed-language-content with nuances surprisingly well to turn web content in the wild into structured data really good and fast.
- lexoj 3mo ago
  I used them because they had the fastest chat response. (Dont think that’s the case anymore, and they introduced some UI blocking feature on load which is irritating, but still use it mainly due to habit)
- jnurmine 3mo ago
  I use Claude with Kiro at work and at home Mistral stuff with pro subscription for coding and research. I don't see a fundamental difference between them in results, at least with what I use them for. The cost is lower too, but it is not the only reason why I won't use Claude at home. Vibe (the CLI Kiro-like tool) feels more "Claude-ish" as it has more terse answers, while the Le Chat can get quite chatty if you really push it ( * ). Prompting it right gets Le Chat more focused and back to being terse. ( * ) Le Chat is by default in "Fast" mode. It also has "Think" and "Research", but I've not felt the need to use those yet. As a practical example: I'm doing some on-and-off family research when I can and have some time since it's the rabbit-holest of all rabbit-holes. I already knew the answers, but decided to test how well Le Chat does. I fed a 208 year old church book page to Le Chat and asked if it can read that handwritten old cursive Swedish and tell me the contents. Le Chat had a look and then explained it could not, but it pointed me to something I had completely missed before, despite having looked for it: The Swedish Lion OCR model by Riksarkivet (Swedish National Archives) which is purpose-built for OCRing such records (the tool by READ-COOP including The Swedish Lion is at http://www.transkribus.org/ http://www.transkribus.org/). Then, Transkribus confirmed my existing information and confirmed that I can kind of sort of read that cursive too. I did not expect any new findings here, just to verify against known facts and things were OK. The tip to Transkribus was very nice and I'll be using that tool more. After this, I asked if Le Chat could dig up some more information about the person (it's a Swedish-Russian noble family connection so a lot of written material exists). Le Chat went about it, summarized real web pages, and the information matched with what I knew already, which was good, no hallucinations or such. I prompted Le Chat further towards the parents and grandparents and so on, it kept on replying with factual summaries and references to web pages that actually exist. This was all in all very good. For what I earlier spent perhaps a weekend or two (taking like two weeks of wall clock time) in total, I could dig up basically the same information, with sources referenced, in a fraction of the time. Even if Le Chat could not read the page, it pointed to Transkribus and that was very helpful. The point is: Mistral performs well for me and I see no reason to use something else. There's also the option to turn off the "use my inputs to learn the model". I don't know if Claude has it or not. Edit: formatting Edit: READ-COOP SCE does the Transkribus
esafak 3mo ago
Is this useful for specifying programs too or only theorems?
- zeckalpha 3mo ago
  Curry-Howard correspondence.
  - esafak 3mo ago
    It may be theoretically possible, but is it ergonomic and useful? Do you use Lean for your programs?
    - tsterin 3mo ago
      use https://rocq-prover.org/ https://rocq-prover.org/ for that purpose
    - nymalt 3mo ago
      I used Lean for AoC last time and it’s really good.
    - siknad 3mo ago
      Lean is intended by its authors to be also used as a general-purpose programming language. Lean stdlib contains an HTTP server for example. IMO the biggest problems are the lack of documentation, instability and poor ecosystem. There are user libraries for some programming tasks (e.g. HTTP router, graphics API bindings) but they are mostly proofs of concept and not actively developed or maintained.
mertleee 3mo ago
[dead]
impodimium 3mo ago
Interesting that this only specialized for Lean4 and not for similar like Coq
- DoctorOetker 3mo ago
  I would have preferred actual proof objects, as in Metamath's: separate the actual proof from the heuristics used to find it (also valuable, but a different thing).
henryrobbins00 3mo ago
What a coincidence! I just released OpenATP earlier today. OpenATP is an open-source Python package and CLI for agentic automated theorem provers. It includes support for Leanstral with Mistral’s Vibe harness. The previous production Leanstral model was deprecated on May 22nd. I will update the package to point to Leanstral 1.5 ASAP! GitHub: https://github.com/henryrobbins/open-atp https://github.com/henryrobbins/open-atp Docs: https://open-atp.henryrobbins.com https://open-atp.henryrobbins.com
pmarreck 3mo ago
Lean 4 and Idris 2 are underrated, and likely great for LLM's to code in (since they provide additional guarantees)
Grimblewald 3mo ago
Got curious, sign up, add money to account, try to use. Can't, it's a labs model. Fine, let's enable labs. Can't, unspecified error. Fine, lets contact customer support as instructed, can't no customer support, just a half-assed FAQ, that seems vibe-coded and searched poorly, totally irrelevant answers coming up for all queries tried. Then it hit me: If AI makes good customer support, then why does no AI company use theirs to provide customer support?
- adithyassekhar 3mo ago
  Because that AI will either expose their business or it will be so nerfed it’s useless.
- tmikaeld 3mo ago
  This isn’t the first time. I’m amazed at how they manage to fumble releases over and over …
- Mashimo 3mo ago
  Further down someone said the support is great and they respond within the day.
  - Grimblewald 3mo ago
    I did get a refund quite quickly, after I finally figured out how to contact their support, which in some stroke of cosmic humor took deepseek to figure out because using their website left my trapped in a dead-end loop. Asking mistral for help lead to links that all 404'd or the same useless help section / faq page.
- saghm 3mo ago
  No one ever thought it made good customer support. It makes cheap customer support, and quite a lot of companies already have shitty customer support because they don't care about it being good, so they're thrilled to get to cut costs further. It's "good" from the perspective of a company that's annoyed to have to spend money on actually fixing things.
- 3mo ago
c7b 3mo ago
I'm not sure I understand the Weights policy. This site says the weights are Apache-licensed, suggesting it's open weights. But I can't find a download link. Their Huggingface profile seems to only provide an earlier snapshot [0]. Any pointers on whether/where we can or will be able to download the weights? [0] https://huggingface.co/mistralai/Leanstral-2603 https://huggingface.co/mistralai/Leanstral-2603
- FranklinChen 3mo ago
  Huh, I haven't found the weights either.
beernet 3mo ago
This went to market horribly (if you can even call it that), just look at the comments. Mistral played themselves big time over the past ~18 months. Non-competitive products and models combined with bad marketing and GTM...Oh Europe
helloplanets 3mo ago
Tangential, but I'm pretty sad about EU having absolutely nothing in the actual SotA LLM market. Especially given the recent events of US completely restricting the actual SotA models. Has this been just pure lack of funding and infra?
- ciefa 3mo ago
  [dead]
- vlian2088 3mo ago
  [flagged]
  - yfontana 3mo ago
    That act applies just as much to those American and Chinese models within the EU.
    - Sol- 3mo ago
      Which is a mistake the EU makes again and again. If you put onerous requirements on everyone, this means that the most well-capitalized firms will be able to shoulder the regulatory overhead the easiest. But who can't? New European startups. This already killed part of the tech sector with the GDPR while Google and Meta just hire 100 lawyers and are done with it.
      - roblabla 3mo ago
        [citation needed] here. The tech sector is still well and alive in EU, and outside adtech (which was hit hard by GDPR - that was the point) doesn't seem to have been visibly impacted.
        mike_hearn 3mo ago
        AI research was mostly funded during the 2010s by Google (funded by ads) and FAIR (Facebook AI Research, funded by ads). Killing off adtech didn't reduce the number of ads seen by people in Europe or make any observable difference to anyone's lives, but did help ensure a company capable of developing LLMs could not arise,
GTP 3mo ago
"Page not found" for me. Did you manage to access this? What is this about?
- sveinbjornp 3mo ago
  from the web archive: Leanstral 1.5 - June 30, 2026 An updated Lean 4 formal proof engineering model optimised for automated theorem proving and autoformalization. 119B total parameters, 6.5B active. https://web.archive.org/web/20260630223430/https://docs.mistral.ai/models/model-cards/leanstral-1-5-26-06 https://web.archive.org/web/20260630223430/https://docs.mist...
butokai 3mo ago
I am getting 404 right now
ramon156 3mo ago
404? https://web.archive.org/web/20260630223430/https://docs.mistral.ai/models/model-cards/leanstral-1-5-26-06 https://web.archive.org/web/20260630223430/https://docs.mist...
Ajoha 3mo ago
Registered due this news. But I must connect to GitHub to use "Code"? That seems limited?

310 points by vetronauta 3mo ago

Discussion about Leanstral 1: https://news.ycombinator.com/item?id=47404796 https://news.ycombinator.com/item?id=47404796

doctorpangloss 3mo ago

Real talk, does anyone use anything from Mistral because it performs the best, by whatever secular metric of your choosing? Or is it only used "because EU"? Just focus on answering the question. I wonder if anyone has observed it perform better on any objective metric in any rigorous setting.

trentor 3mo ago
I like the models for creative writing. They have a distinct voice that is different from the other llms.
- SwellJoe 3mo ago
  I made a game (https://prose-or-con.com https://prose-or-con.com) where you pick whether writing is AI or human. Mistral is a bonkers weird writer. So weird I fell for it a couple of times because I thought, "No way a model writes this weird." Not, like, incorrect grammar or spelling or anything, just...off-kilter. Kinda sassy.
  - vlian2088 3mo ago
    needs a leaderboard of models most often mistaken for humans.
    - SwellJoe 3mo ago
      Yes, it's on the todo list, but I need more data. Only a half dozen people have played it and submitted a score. I'm storing the hashes of passages people got right and wrong so I can make exactly that chart at some point. I think both "the most human-like AI" and "the most AI-like human" are both interesting pieces of data, but I don't know either yet.
      - vlian2088 3mo ago
        try posting it on r/localllama and r/sillytavernai
troyvit 3mo ago
We are not Mistral's target audience. For instance I don't know if Leanstral performs the best as a "formal proof engineering model optimised for automated theorem proving and autoformalization" because I don't even know wth that is or who else does it. Mistral themselves focus more on b2b; financial services, manufacturing, stuff like that, and they get some big clients that way. Despite not being their target, I started using them because they have many open models. I continue using them because, yeah EU, but also because the community is great and the tool makes me think more than Claude does. Last, I stick with them because they are one of the few AI companies that are up-front about their environmental impact and are actually trying to minimize it while still providing a decent product.
- computerex 3mo ago
  It's for mathematics. There is this programming language: https://lean-lang.org/ https://lean-lang.org/ If you can express a solution in Lean you can formally prove or disprove it. Formal verification is making a debut in traditional engineering toolkits.
data-ottawa 3mo ago
Mistral medium is considerably better at writing than Opus. I’ve also found it very good at pulling info from pdfs. Even a complicated festival with multiple venues and timetables.
- tjwebbnorfolk 3mo ago
  Writing what? I found it worse than gemma4 at coding even though it's 4x the parameter size
Adrig 3mo ago
A few months ago, I had some data cleaning to do; their small model was surprisingly efficient and got the job done for 0.2x what I expected to run (Anthropic Sonnet / Haiku). Their TTS / STT is also roughly at the frontier, at least for French. But I admit I only consider them because they're from France. Haven't seen a dimension where they're competitive for general users
evilmonkey19 3mo ago
I use it because EU and API pricing is decent to me. And support is awesome also. They reply the same day or at most the next day, and they follow the ticket great. It isn't that bad, but neither the best.
- jatora 3mo ago
  Why do you need support so often?
adev_ 3mo ago
> Mistral because it performs the best, by whatever secular metric of your choosing? I am. I use them primarily through their vibe CLI. Reason is simple: They are cheaper (by almost one order of magnitude compared to Claude) and still do the job pretty well. For small programming tasks, quick prototyping, refactoring or anything verbose and not requiring a context too large: I first go to Mistral and then eventually to Claude if I'm unsatisfied. I also found out some of their models to be more responsive than OpenAI ones (which is not so surprising considering the size). My tasks are mainly C++ and Python programming. People in other languages might not share my enthusiasm.
- jatora 3mo ago
  Your reason can't be cost because there are superior models that are cheaper than Mistral models, for coding. So i re-ask the question
  - adev_ 3mo ago
    > Your reason can't be cost because there are superior models that are cheaper than Mistral models Nope. This is not my experience. Public pricing in token/$ is only part of the equation. Mistral tooling to consume significantly less tokens-per-given-task than the Anthropic ones. My bills currently reflects that.
    - tjwebbnorfolk 3mo ago
      I think other commenter is talking about smaller/cheaper models like Qwen that outperform mistral on just about every metric
      - adev_ 3mo ago
        I played with Qwen few months ago, I do prefer Mistral vibe for everyday usage (significantly faster if not self hosted).
    - greenavocado 3mo ago
hakunin 3mo ago
I use it because it’s a simple, convenient and cheap OCR api. Specifically via my ringbinder[1] tool. [1]: https://github.com/maxim/ringbinder https://github.com/maxim/ringbinder
Confiks 3mo ago
For writing and languange learning it's very decent, especially Mistral Large. The pricing is very good too. I really like the consistently low time to first token and good token per second. Claude, especially in the past, would be very inconsistent, often with outages. Mistral mostly just always works and is very fast. Technical questions are unfortunately hit or miss. I'm lately pretty much always using a system prompt that emphasizes short answers [1], and Opus regularly one-shots it while Mistral needs a follow up. I use big-AGI as a model router [2] (dumb name, great software), which makes switching midway very easy though. For coding I'm still using Claude Code mostly out of inertia (although I really want to move to an OSS harness) and the one time I tried their `vibe` tool months ago it was a bit rough. Mistral TTS with diarization is also great and cheap. That's the only thing for which I use their web UI. [1] Give a short but helpful answer to the question the user asks. When helping with a computer-related task, unless the user asks, don't give any installation or setup instructions, but just get straight to the point. When the user asks a follow up question, give a more complete and longer answer while still not overexplaining. When the user prefaces the question with "short mode off" in any question, give a full and well considered reply. [2] https://github.com/enricoros/big-AGI https://github.com/enricoros/big-AGI
- Skinney 3mo ago
  vibe has improved _a lot_ during the past few months, fyi. The new Mistral Medium 3.5 is also a big improvement over devstral-2
- BartjeD 3mo ago
  Mistral doesn't have caching on batches. For me that meant they are 10x more expensive than Google. I think its dumb. Their support is hidden away in a chat bubble at the bottom. But they do respond promptly. Its decent, but after switching to Google i wouldn't go back
ashenke 3mo ago
I use their Voxtral Mini STT audio model to automatically transcribe my podcasts into markdown. Out of all the STT models I've tried, it's both the best performing and one of the cheapest! It's really accurate, feeding the episode notes and the podcast description ensures all names are properly spelled, and speaker diarization works really great. (I just do a Gemini flash pass at the end to identify the speakers, so it shows the host name instead of "Speaker 1")
refulgentis 3mo ago
OCR is off the charts good on every metric you can think of. LLMs are a near-afterthought at this point if you don’t have data residency requirements. I love them and they’re slightly underrated, their models are consistently well-trained, open, but as you note, behind. There is no metric that will say they’re ahead in anything.
- cavenditti 3mo ago
  This. Best OCR provider by measure and it’s been for years
  - urbsgpw 3mo ago
    Hmm, not sure I'd agree. I really like google's offering there (they suck at coding agents but their OCR is good value for money - well up till the latest flash model which has got wicked expensive). See also https://www.ocrarena.ai/leaderboard https://www.ocrarena.ai/leaderboard I know these leaderboards are iffy, but at least my experience has been somewhat similar.
    - refulgentis 3mo ago
      Thank you for sharing this, I’ve had some disquiet around the release blogs…something felt cherry-picked and I didn’t know there was a 3rd party source for evals, that settles it easily - like you said they can be iffy but there’s a clear enough gap and large set of models for me to let go of the idea it’s the best by some margin.
suprjami 3mo ago
I still prefer Mistral Nemo 12B for text summarisation tasks. It has a nice style. The Mistral Small 24B is also decent. I have a YouTube transcript summariser which I like these for. However these days I usually have Qwen 3.6 27B already loaded so I mostly just use that instead.
bee_rider 3mo ago
I liked that their website didn’t ask for my phone number, IIRC.
Hamuko 3mo ago
>Just focus on answering the question. Are you trying to instruct me like an LLM?
psalaun 3mo ago
I use it as my workhorse for coding and general chat questions, because it's good enough 80% of the time, and indeed it's french/european (with heavy US capital tho...). We complain too much about not having enough major competitors in the IT space, to not support a burgeoning one even if it's less powerful than SOTA labs
- barrenko 3mo ago
  Well, if you're a taxpayer in EU you're already supporting it implicitly.
istinetz 3mo ago
For a defense project we're working on, we basically have a hard requirement to use european cloud provider + european llm We cannot use open source LLMs on-prem, I asked. So that's basically a hard requirement to use mistral, even though Chinese models are strictly better on every dimension.
- angry_octet 3mo ago
  Is there a rationale behind why not on prem? Boogeyman fears about LLMs? No hardware? Or do you mean, no Chinese LLMs?
anonyfox 3mo ago
just used mistral for a database/scraping creation tool and ended at <10k€ in token costs (via openrouter), beating gpt5.4-mini in output quality and speed and costs after actual testing A/B fairly. so its a super scoped task to be performed hundreds of thousands of time for some automation and mistral just did it better across all dimensions that gpt-5.4-mini. of course thats not a headline in terms of frontier model competitiveness, but for "the boring parts" it just was flat out better than anything else consistently. bonus points it handles mixed-language-content with nuances surprisingly well to turn web content in the wild into structured data really good and fast.
lexoj 3mo ago
I used them because they had the fastest chat response. (Dont think that’s the case anymore, and they introduced some UI blocking feature on load which is irritating, but still use it mainly due to habit)
jnurmine 3mo ago
I use Claude with Kiro at work and at home Mistral stuff with pro subscription for coding and research. I don't see a fundamental difference between them in results, at least with what I use them for. The cost is lower too, but it is not the only reason why I won't use Claude at home. Vibe (the CLI Kiro-like tool) feels more "Claude-ish" as it has more terse answers, while the Le Chat can get quite chatty if you really push it ( * ). Prompting it right gets Le Chat more focused and back to being terse. ( * ) Le Chat is by default in "Fast" mode. It also has "Think" and "Research", but I've not felt the need to use those yet. As a practical example: I'm doing some on-and-off family research when I can and have some time since it's the rabbit-holest of all rabbit-holes. I already knew the answers, but decided to test how well Le Chat does. I fed a 208 year old church book page to Le Chat and asked if it can read that handwritten old cursive Swedish and tell me the contents. Le Chat had a look and then explained it could not, but it pointed me to something I had completely missed before, despite having looked for it: The Swedish Lion OCR model by Riksarkivet (Swedish National Archives) which is purpose-built for OCRing such records (the tool by READ-COOP including The Swedish Lion is at http://www.transkribus.org/ http://www.transkribus.org/). Then, Transkribus confirmed my existing information and confirmed that I can kind of sort of read that cursive too. I did not expect any new findings here, just to verify against known facts and things were OK. The tip to Transkribus was very nice and I'll be using that tool more. After this, I asked if Le Chat could dig up some more information about the person (it's a Swedish-Russian noble family connection so a lot of written material exists). Le Chat went about it, summarized real web pages, and the information matched with what I knew already, which was good, no hallucinations or such. I prompted Le Chat further towards the parents and grandparents and so on, it kept on replying with factual summaries and references to web pages that actually exist. This was all in all very good. For what I earlier spent perhaps a weekend or two (taking like two weeks of wall clock time) in total, I could dig up basically the same information, with sources referenced, in a fraction of the time. Even if Le Chat could not read the page, it pointed to Transkribus and that was very helpful. The point is: Mistral performs well for me and I see no reason to use something else. There's also the option to turn off the "use my inputs to learn the model". I don't know if Claude has it or not. Edit: formatting Edit: READ-COOP SCE does the Transkribus

esafak 3mo ago

Is this useful for specifying programs too or only theorems?

zeckalpha 3mo ago
Curry-Howard correspondence.
- esafak 3mo ago
  It may be theoretically possible, but is it ergonomic and useful? Do you use Lean for your programs?
  - tsterin 3mo ago
    use https://rocq-prover.org/ https://rocq-prover.org/ for that purpose
  - nymalt 3mo ago
    I used Lean for AoC last time and it’s really good.
  - siknad 3mo ago
    Lean is intended by its authors to be also used as a general-purpose programming language. Lean stdlib contains an HTTP server for example. IMO the biggest problems are the lack of documentation, instability and poor ecosystem. There are user libraries for some programming tasks (e.g. HTTP router, graphics API bindings) but they are mostly proofs of concept and not actively developed or maintained.

mertleee 3mo ago

[dead]

impodimium 3mo ago

Interesting that this only specialized for Lean4 and not for similar like Coq

DoctorOetker 3mo ago
I would have preferred actual proof objects, as in Metamath's: separate the actual proof from the heuristics used to find it (also valuable, but a different thing).

henryrobbins00 3mo ago

What a coincidence! I just released OpenATP earlier today. OpenATP is an open-source Python package and CLI for agentic automated theorem provers. It includes support for Leanstral with Mistral’s Vibe harness. The previous production Leanstral model was deprecated on May 22nd. I will update the package to point to Leanstral 1.5 ASAP! GitHub: https://github.com/henryrobbins/open-atp https://github.com/henryrobbins/open-atp Docs: https://open-atp.henryrobbins.com https://open-atp.henryrobbins.com

pmarreck 3mo ago

Lean 4 and Idris 2 are underrated, and likely great for LLM's to code in (since they provide additional guarantees)

Grimblewald 3mo ago

Got curious, sign up, add money to account, try to use. Can't, it's a labs model. Fine, let's enable labs. Can't, unspecified error. Fine, lets contact customer support as instructed, can't no customer support, just a half-assed FAQ, that seems vibe-coded and searched poorly, totally irrelevant answers coming up for all queries tried. Then it hit me: If AI makes good customer support, then why does no AI company use theirs to provide customer support?

adithyassekhar 3mo ago
Because that AI will either expose their business or it will be so nerfed it’s useless.
tmikaeld 3mo ago
This isn’t the first time. I’m amazed at how they manage to fumble releases over and over …
Mashimo 3mo ago
Further down someone said the support is great and they respond within the day.
- Grimblewald 3mo ago
  I did get a refund quite quickly, after I finally figured out how to contact their support, which in some stroke of cosmic humor took deepseek to figure out because using their website left my trapped in a dead-end loop. Asking mistral for help lead to links that all 404'd or the same useless help section / faq page.
saghm 3mo ago
No one ever thought it made good customer support. It makes cheap customer support, and quite a lot of companies already have shitty customer support because they don't care about it being good, so they're thrilled to get to cut costs further. It's "good" from the perspective of a company that's annoyed to have to spend money on actually fixing things.
3mo ago

c7b 3mo ago

I'm not sure I understand the Weights policy. This site says the weights are Apache-licensed, suggesting it's open weights. But I can't find a download link. Their Huggingface profile seems to only provide an earlier snapshot [0]. Any pointers on whether/where we can or will be able to download the weights? [0] https://huggingface.co/mistralai/Leanstral-2603 https://huggingface.co/mistralai/Leanstral-2603

FranklinChen 3mo ago
Huh, I haven't found the weights either.

beernet 3mo ago

This went to market horribly (if you can even call it that), just look at the comments. Mistral played themselves big time over the past ~18 months. Non-competitive products and models combined with bad marketing and GTM...Oh Europe

helloplanets 3mo ago

Tangential, but I'm pretty sad about EU having absolutely nothing in the actual SotA LLM market. Especially given the recent events of US completely restricting the actual SotA models. Has this been just pure lack of funding and infra?

ciefa 3mo ago
[dead]
vlian2088 3mo ago
[flagged]
- yfontana 3mo ago
  That act applies just as much to those American and Chinese models within the EU.
  - Sol- 3mo ago
    Which is a mistake the EU makes again and again. If you put onerous requirements on everyone, this means that the most well-capitalized firms will be able to shoulder the regulatory overhead the easiest. But who can't? New European startups. This already killed part of the tech sector with the GDPR while Google and Meta just hire 100 lawyers and are done with it.
    - roblabla 3mo ago
      [citation needed] here. The tech sector is still well and alive in EU, and outside adtech (which was hit hard by GDPR - that was the point) doesn't seem to have been visibly impacted.
      - mike_hearn 3mo ago
        AI research was mostly funded during the 2010s by Google (funded by ads) and FAIR (Facebook AI Research, funded by ads). Killing off adtech didn't reduce the number of ads seen by people in Europe or make any observable difference to anyone's lives, but did help ensure a company capable of developing LLMs could not arise,

GTP 3mo ago

"Page not found" for me. Did you manage to access this? What is this about?

sveinbjornp 3mo ago
from the web archive: Leanstral 1.5 - June 30, 2026 An updated Lean 4 formal proof engineering model optimised for automated theorem proving and autoformalization. 119B total parameters, 6.5B active. https://web.archive.org/web/20260630223430/https://docs.mistral.ai/models/model-cards/leanstral-1-5-26-06 https://web.archive.org/web/20260630223430/https://docs.mist...

butokai 3mo ago

I am getting 404 right now

ramon156 3mo ago

404? https://web.archive.org/web/20260630223430/https://docs.mistral.ai/models/model-cards/leanstral-1-5-26-06 https://web.archive.org/web/20260630223430/https://docs.mist...

Ajoha 3mo ago

Registered due this news. But I must connect to GitHub to use "Code"? That seems limited?