Discussion summary
The discussion highlights Europe's lag in AI development compared to North America, with some noting the US's less desirable environment. Participants discuss the capabilities of Leanstral 1.5 with 6B parameters and compare it to larger models like GPT-5.5, emphasizing the importance of mechanisms over size.
What the discussion says
- Europe is behind in AI progress and may not recover easily.
- US offers higher pay but worse living conditions, making it less attractive.
- Leanstral 1.5 with 6B parameters is notable, but GPT-5.5 has more parameters.
- Some see value in mechanisms and tools over sheer model size.
“Europe is far behind, and the gap might be irrecoverable.”
“Treating AI models better doesn't necessarily mean earning more.”
Join the discussion
Write your take first — we'll ask for email only when you're ready to publish.
- Hacker News
- Discussed the other day:by andai
- 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?by raphinou
- Curious 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?by RossBencina
- I find it a bit ridiculous to be critisizing Mistral, of all companies, as falling behind the Frontier models.
Firstly, who hasn't fallen behind? Grok...Meta....? A lot of big companies are struggling.
Secondly, Mistral are trying to solve a different problem.
Finally, Mistral should be congratulated for staying in the race for so long now.
by bjt12345 - >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 before this was published: https://github.com/datrs/varinteger/issues/8 (is this a leanstral employee? they have almost no info and only very sparse activity. or did leanstral perhaps just pick up this issue?)
it's a tiny, surprisingly-poorly tested, long-untouched (8y) library: https://github.com/datrs/varinteger/blob/master/tests/test.r... that has about 1k downloads per day: https://crates.io/crates/varinteger [1] which seems rather low.
I don't think I'd consider that such a smashing success that it's worth bringing up as the sole example tbh. though automated detection is certainly useful. or is this a noteworthy accomplishment for this sub-field? I haven't played with proof-writing LLMs, but given the paucity of training data I wouldn't be surprised if they're a bit rough compared to general coding.
1: https://crates.io/crates/varinteger lists it as https://github.com/mafintosh/varinteger-rs which redirects to https://github.com/datrs/varinteger , so despite looking different at a glance it does appear to be the same library
by Groxx - Halfway 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.by andai
- This 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 that "testing [...] would typically miss"? It's certainly something that bad tests would miss or not think about, but I find that (a) careful people and (b) ML coding systems are actually really good at "oh, I should test the extreme values". Especially for things that parse user input.
I'm curious if they found other bugs that were more interesting, but found them too hard to explain quickly.
by boulos - There'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.