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.

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.