61–70 of 116 posts
Earlier quoted context omitted.
Stupid Europoors, optimizing for making a good product, instead of optimizing for making as much money as possible /s
big AI labs make so much money because they have a good (amazing) product
Earlier quoted context omitted.
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.
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…
Plus, you can't really build loyalty on a 100 USD/Y price tag. Since there are no switching costs holding them back, those buyers will leave the moment somebody offers a lower rate. An easily cloned, low cost tool with zero customer lock in is not a business. It is a feature.
That might sound great for the buyer (you), but it is a terrible strategy if we want a European company to compete long term against global competitors on actual product merit instead of just regulatory arbitrage.
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?
I still have a ways to go before calling myself a lean4 expert, but I don't need assist to get useful programs anymore.
The ability to start with very little knowledge and still be able to trust parts you don't fully understand is a real unlock on learning progress: it's both practical and motivating to get useful programs you can rely on with incomplete knowledge, it sort of drags you in. You're bounded by the subset of the language that describes your axiom and proposition surface, not the subset that describes the intermediate steps. Over time as your ambition goes up, you need to understand more to do more things, but you can operate safely at level N+1 in a sense.
It's also just a delightful programming language irrespective of its theorem proving role, and it's remarkably fast. I've got it bolted to io_uring and in many cases it blows the ass off of C++ with libuv or Rust with Tokio. Now and again you'll see some huge tail at the p99.99 latency or something and you go make a number fixed width or something, but you have to tune C++ and Rust too.
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…
I'm not sure the "a year of document processing for under 100 USD/y" is such as great thing as you think it is (at least not for European competitiveness)... It means Mistral is essentially setting a revenue ceiling very low. OCR is a commodity at this point, and open source models, AWS, etc already do it out of the box. Plus, you can't really build loyalty on a 100 USD/Y price tag. Since there are no switching costs…
And yes, its good that "its good for buyer" after all we do business so that living would be nicer, not the other way around (live to do business)
Earlier quoted context omitted.
Stupid Europoors, optimizing for making a good product, instead of optimizing for making as much money as possible /s
big AI labs make so much money because they have a good (amazing) product
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…
But how does it compete on OCR? I find that having good quality at a cheap price is more niche than having the best quality at 10x the cheap price, because for most use cases you want to pay a bit more if it saves you mistakes later.
Basically, to find the answer you really need your own benchmark you run with real examples from what you want to do. Basically the same goes for anything ML nowadays as the public benchmarks cannot really be trusted to give you any sort of indication on how we'll it'd work for you.
Earlier quoted context omitted.
big AI labs make so much money because they have a good (amazing) product
Big AI labs aren't making money. They're buying revenue. Sure, the product is amazing, but it wouldn't be as amazing if offered at cost - which is exactly where "good enough" smaller and specialized models will survive.
And API is 80% of their business (subscriptions the other 20%)
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…
I'm not sure the "a year of document processing for under 100 USD/y" is such as great thing as you think it is (at least not for European competitiveness)... It means Mistral is essentially setting a revenue ceiling very low. OCR is a commodity at this point, and open source models, AWS, etc already do it out of the box. Plus, you can't really build loyalty on a 100 USD/Y price tag. Since there are no switching costs…
Earlier quoted context omitted.
It's really good. I didn't do any type of statistical evaluation or comparison to other models, but it's so good that it doesn't matter to me if there's an option that might be even better.
curious if you tried local LLM models for OCR, like a Gemma4, or your volume is too much for that