Leanstral 1.5 is a what..?

I was doing the do out on the internet, as you do, and came across Mistral AI Leanstral 1.5. Which calls itself:

An updated Lean 4 formal proof engineering model optimised for automated theorem proving and autoformalization. 119B total parameters, 6.5B active.

I was like, wow, thats a thingymabob of the 1st order. The last time someone said "formal methods" to me was in 1998, a bloke called Paul in a computer lab in Surrey. I had not a Scooby Doo what that was, and here we are more than a quarter of a century later, and solving something cool with formal methods is still on my bucket list. Boo hoo.

I had to check the blog to ask what-the-actual-fluff all this i about Leanstral 1.5: Proof Abundance for All. They are letting you use it for FREE. So you can go wild having it formally prove you don't have bugs in your mission-critical systems code! Yipee! 🎉

Well, it turns out I need a formal proof that my Unbounded Viewstamped Replication Revisited code doesn't have many problems. So I thought I'd ask Fable 5.1, GPT 6 and GLM-5.3-Flash to kick the tyres on getting the Leanstral model to write out formal proofs in pretty Greek characters and debug it. Huh, you did what!?

Well, let's say a model was not good at, I dunno, coding in a rare language, like Felienne Hermans’ Hedy. You could fine-tune a model on that and make a language server that lints the code so that a special model trained on a fast set of examples can happily write code in Arabic and right-to-left with all the different and rare Arabic numerals. That would be so darn cool.

Well, Mistral AI have done that for the LeanProver language Lean. They have a VS Code Plugin. On their blog, they show Claude can find real solutions to real problems, but at a high cost. I told Claude to call Leanstral if it needed help writing Lean4 proofs it could solve. Which it duly did when it got a bit stuck. Here is what it wrote:

So now I need to figure out what all that means, as it's talking about Rust code in Lean4, and whether it is valid, or something!

If only I had a time machine to go back and talk to Paul, since he is probably the only person who is gonna think this is really darn cool!