Can this be useful for someone with no prior knowledge of lean? I'd like to verify a software I'm working on, but I have no experience in formal verification. Can I get useful result with the spec, the code and some (limited) learning time on my side?
Leanstral 1.5: Proof abundance for all
41–50 of 116 posts
Re: Leanstral 1.5: Proof abundance for all
#42Can this be useful for someone with no prior knowledge of lean? I'd like to verify a software I'm working on, but I have no experience in formal verification. Can I get useful result with the spec, the code and some (limited) learning time on my side?
I think at minimum you would need to understand which theorems you want to prove about your code, and how to express those in Lean. Otherwise you won’t be able to verify the output. It may have proven some statement that is machine checked to be correct, but it’s pointless if you don’t understand what that statement means and if it covers what you want to verify about your code.
Re: Leanstral 1.5: Proof abundance for all
#43I applaud mistral's efforts but reading this release made me realize that Europe is far far behind and that once the gap is solidified I don't think its recoverable in the same way Canada's brain drain had on its economy The best and the brightest from Europe have no incentive to build in Europe when they can do it in America and be compensated and treated far better
Fortunately for Europe, the US is doing its best to make itself both an undesirable and unavailable immigration target.
Re: Leanstral 1.5: Proof abundance for all
#44I applaud mistral's efforts but reading this release made me realize that Europe is far far behind and that once the gap is solidified I don't think its recoverable in the same way Canada's brain drain had on its economy The best and the brightest from Europe have no incentive to build in Europe when they can do it in America and be compensated and treated far better
At this point I wouldn’t move to USA if you paid me double the salary. There are more things in life than money. That said, if (or when) the progress of the LLMs flatten out, then I think even Europe can catch up in a few years. If they don’t, and that seems unlikely to me, if the required compute needs to increase at the rate it does today, then I am not sure any of us can predict where society ends up.
I think there is a non-zero chance that Europe stumbled into an optimal scenario where they avoided all the losses incurred by US companies, but still benefit from the research. Having said that, doing so would require moving at the exact right time.
Re: Leanstral 1.5: Proof abundance for all
#45I gave Codex with GPT-5.5 High this prompt: Identify bugs in [datrs/varinteger](https://github.com/datrs/varinteger) . Do NOT look at the GitHub issues, just inspect the source It also found the bug that Leanstral 1.5 found and the authors highlighted. I think this bug wasn't especially tricky; it's just a case of too few eyeballs on this repo. Congrats on the release regardless! Excited for the direction Lean + auto…
GPT-5.5 is what, a trillion+ parameter model? I think the insight here is that you can do this with a tiny model.
Re: Leanstral 1.5: Proof abundance for all
#46There's a lot of criticism of Mistral being unable to compete with large model, and that's fair. But I think it dismisses what Mistral is actually doing, which is making specific capabilities available at high quality in tiny models.
I do a lot of OCR, file analysis, stuff like that. I use Mistral for that. I put 100$ into my account, and it just runs for a year without any worries about the amount of requests I make, because the cost is minuscule. That's valuable, even if it doesn't compete with Opus 4.8.
Re: Leanstral 1.5: Proof abundance for all
#47Can this be useful for someone with no prior knowledge of lean? I'd like to verify a software I'm working on, but I have no experience in formal verification. Can I get useful result with the spec, the code and some (limited) learning time on my side?
Read this section of the article “ Bug Discovery: Finding Hidden Flaws”, they appear to have used the model on open source Rust to find issues starting with just the Rust code.
You might be also able to have conversations that help you write the Lean to verify your application, but I’m not certain about this.
Re: Leanstral 1.5: Proof abundance for all
#48Was fun to see their developers make nods to Le Chaton Fat in the announcements for this on Twitter.
I suspect a true "big new general-purpose" model is around the corner from them, whether or not they were in on Le Chaton Fat for real. They've mentioned it after the media circus. Hopefully more creatively named than just "Large 4".
Re: Leanstral 1.5: Proof abundance for all
#49I applaud mistral's efforts but reading this release made me realize that Europe is far far behind and that once the gap is solidified I don't think its recoverable in the same way Canada's brain drain had on its economy The best and the brightest from Europe have no incentive to build in Europe when they can do it in America and be compensated and treated far better
At this point I wouldn’t move to USA if you paid me double the salary. There are more things in life than money. That said, if (or when) the progress of the LLMs flatten out, then I think even Europe can catch up in a few years. If they don’t, and that seems unlikely to me, if the required compute needs to increase at the rate it does today, then I am not sure any of us can predict where society ends up.
Sure some people like to make less money and pay more taxes for ideological reasons. I respect that.
Re: Leanstral 1.5: Proof abundance for all
#50I applaud mistral's efforts but reading this release made me realize that Europe is far far behind and that once the gap is solidified I don't think its recoverable in the same way Canada's brain drain had on its economy The best and the brightest from Europe have no incentive to build in Europe when they can do it in America and be compensated and treated far better
treated far better != earn more money