Is this useful for specifying programs too or only theorems?
Leanstral 1.5
11–20 of 158 posts
Re: Leanstral 1.5
#12Real 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.
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 st…
It's for mathematics. There is this programming language:
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.
Re: Leanstral 1.5
#13Is this useful for specifying programs too or only theorems?
Curry-Howard correspondence.
Re: Leanstral 1.5
#14Real 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.
I use it because it’s a simple, convenient and cheap OCR api. Specifically via my ringbinder[1] tool.
Re: Leanstral 1.5
#15Real 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.
> 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…
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
Re: Leanstral 1.5
#16Real 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.
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.
Why do you need support so often?
Re: Leanstral 1.5
#17Real 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.
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.
Re: Leanstral 1.5
#18Earlier quoted context omitted.
> 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…
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
> 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.
Re: Leanstral 1.5
#19Real 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.
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")
Re: Leanstral 1.5
#20[dead]