[dupe] https://news.ycombinator.com/item?id=48738938
Have you ever been downvoted for calling 'dupe?' I once was downvoted after calling dupe on a link posted thrice. HN is an interesting place to hang out, that's for sure.
Leanstral 1.5: Proof abundance for all
31–40 of 116 posts
Re: Leanstral 1.5: Proof abundance for all
#32Earlier 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!
[deleted]
Re: Leanstral 1.5: Proof abundance for all
#33Earlier 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!
You know, I was going to reply to the person who called out your comment as an "ad", because I visited the site and it's actually relevant to the topic under discussion (Leanstral). And not even selling anything.
My thought was: Good job, this is tasteful personable marketing for a product with genuine value. I wish more marketing were done this way. So I think it's totally fine to be talking about the cool thing you're working on. I for one found it interesting and added to the discussion.
Re: Leanstral 1.5: Proof abundance for all
#34I 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…
Leanstral 1.5 has 6B active parameters. How many parameters does GPT-5.5 have?
We can run Leanstral locally on commodity/consumer hardware. Nuff said.
Re: Leanstral 1.5: Proof abundance for all
#35This is nice work, but I found the bug finding example to be weird: > 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. In what way would this boundary condition case be considered something…
Because this is garbage PR. That's it.
Every property-based testing system (invented ca. 1980) will explore boundary values. The semantics (or lack thereof) of C and C++ can make this difficult to actually test for because the compiler is allowed to say "test passed" to any input leading to UB.
Re: Leanstral 1.5: Proof abundance for all
#36Halfway 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.
It’s a 6bn model. Totally different class. I’m more excited about “frontier small language models” tbh.
Re: Leanstral 1.5: Proof abundance for all
#37This is nice work, but I found the bug finding example to be weird: > 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. In what way would this boundary condition case be considered something…
Because this is garbage PR. That's it. Every property-based testing system (invented ca. 1980) will explore boundary values. The semantics (or lack thereof) of C and C++ can make this difficult to actually test for because the compiler is allowed to say "test passed" to any input leading to UB.
Property based testing is good at generating boundary values for inputs. But for any more complicated piece of code getting boundary value coverage of interior values is an open problem that requires instrumentation feedback to understand branch coverage and value coverage of the code that got tested. It’s not an easy thing at all.
Re: Leanstral 1.5: Proof abundance for all
#38Earlier 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!
Your comment is helpful, useful, and relevant. Please keep going.
Just my 2c, but maybe your original post could’ve been written in a less promotional / less excited way. It looked a little like spam at _first_ glance.
Re: Leanstral 1.5: Proof abundance for all
#39I 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.
Re: Leanstral 1.5: Proof abundance for all
#40I 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
[flagged]