Leanstral 1.5

(docs.mistral.ai)

74 points | by vetronauta 3 hours ago

3 comments

  • __natty__ 1 hour ago
    Discussion about Leanstral 1: https://news.ycombinator.com/item?id=47404796
  • esafak 3 minutes ago
    Is this useful for specifying programs too or only theorems?
  • doctorpangloss 59 minutes 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.
    • troyvit 40 minutes 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 2 minutes ago
        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.

    • adev_ 10 minutes 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.

    • evilmonkey19 20 minutes 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.
    • data-ottawa 38 minutes 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.

    • trentor 50 minutes ago
      I like the models for creative writing. They have a distinct voice that is different from the other llms.
      • SwellJoe 34 minutes ago
        I made a game (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.
    • Adrig 37 minutes 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