[flagged]
Leanstral 1.5: Proof abundance for all
21–30 of 116 posts
Re: Leanstral 1.5: Proof abundance for all
#22Re: Leanstral 1.5: Proof abundance for all
#23> One such bug was in the sign function for zigzag decoding of the datrs/varinteger library. On input Std.U64.MAX, the expression (value + 1) overflowed, causing crashes in debug mode and silent corruption in release mode—an edge case that testing and fuzzing would typically miss. that library is: https://github.com/datrs/varinteger it seems probably correct, as there's an identical issue filed on that repo a week be…
The problem with proof is that it’s a bit hard sometimes to convey the value. The point is not to find bugs, but to prove that there are none (of a certain class; under certain assumptions; etc). But it’s a hard story to sell, so often the marketing is around “look at this bug we found”.
Re: Leanstral 1.5: Proof abundance for all
#24I 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…
Given that they directly compare to GPT-5.5 in their documentation. This comes off as puppy kicking to me. They state it is not SOTA, even IN its domain!
Honestly: Think twice before dragging your firm into what you say.
Disclaimer: I speak for myself. Not any firm I am associated with.
Re: Leanstral 1.5: Proof abundance for all
#25> One such bug was in the sign function for zigzag decoding of the datrs/varinteger library. On input Std.U64.MAX, the expression (value + 1) overflowed, causing crashes in debug mode and silent corruption in release mode—an edge case that testing and fuzzing would typically miss. that library is: https://github.com/datrs/varinteger it seems probably correct, as there's an identical issue filed on that repo a week be…
The problem with proof is that it’s a bit hard sometimes to convey the value. The point is not to find bugs, but to prove that there are none (of a certain class; under certain assumptions; etc). But it’s a hard story to sell, so often the marketing is around “look at this bug we found”.
I would be much more interested in "here is a provably memory safe version of openssl with all its memory safety bugs fixed"
Re: Leanstral 1.5: Proof abundance for all
#26I 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…
> It also found the bug that Leanstral 1.5 found and the authors highlighted
This is a little bit like someone pointing the moon and you look at the finger.
The formal proof domain goes way beyond just finding bugs.
It has tons of usages in term of functional safety, protocol validation, cryptography, etc...
The fact Mistral tackle this kind of problem is both smart and not so surprising.
Smart because it is niche enough that they do not front face the big competitors (yet).
No so surprising because the French labs have a well known and long time expertise with formal proof tools (Coq and all its Ocaml associated tools). It has been historically mainly pushed by the aerospace and train industries (Airbus, Dassault, Alsthom).
Re: Leanstral 1.5: Proof abundance for all
#27Curious that they are pitching Lean 4 for formal verification. I thought that this was more the domain of Isabelle/HOL and TLA+. At least I would have expected a model trained at using all three. Maybe also Isabell/Isar, which seems preferable for forward derivations in linear algebra. Could anyone shed some light on this?
It is true that Lean has seen relatively little adoption in software verification compared to e.g. Isabelle and Rocq (previously Coq). Even Agda has had more traction in that domain.
However, Lean is currently gaining significant momentum as an alternative, particularly due to its capabilities as a general-purpose functional programming language.
Personally, I think something based on Hoare or separation logic would be more practical as it'd be easier to align requirements with specifications. I like Dafny and F*.
Re: Leanstral 1.5: Proof abundance for all
#28Halfway thru the article it shows a comparison with several frontier-ish LLMs. But they're all from half a year ago. "Our new model is better than all these Chinese models from 3 generations ago" is pretty funny to me.
Agreed, though open weights + relatively small is still headline worthy. This thing really cooks.
Re: Leanstral 1.5: Proof abundance for all
#29I 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
Re: Leanstral 1.5: Proof abundance for all
#30Earlier quoted context omitted.
[flagged]
Earnest question: any recommendation to not come off this way in forums? I created this tool for my own research and have found it really helpful to benchmark different automated theorem provers (my experience so far has been that Claude Code + Codex still out-perform Leanstral). My genuine aim is to share that usefulness with others, not self promote!
I don't know why but sometime ago, HN started resembling reddit, and there seems to be just widespread fear/jealousy/cynicism towards anybody advertising their work or services even, I don't think there was anything wrong with your post, it was informative.
Probably the most annoying part about Reddit and HN and X (although it let you mute people) is the abundance of "expert" opinions from people who aren't experts at all. You just end up with a bunch of false signals that you shouldn't even be listening to.
all in all I say invest in spreading the words via other channels, maybe even X is better and even the right time zone (besides US working hours, I find European time the worst statistically for sharing your work).