71–80 of 116 posts
Earlier quoted context omitted.
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.
Anthropic is selling API tokens at 80% margin. And API is 80% of their business (subscriptions the other 20%)
> 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”.
Now, go write the code for an artificial heart , and sleep at night thanks to strong testing !
Earlier quoted context omitted.
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.
Anthropic is selling API tokens at 80% margin. And API is 80% of their business (subscriptions the other 20%)
Earlier quoted context omitted.
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…
well all commodities are like this. replace AI with milk, or plastic. It's easy for me to just move to different milk provider, this does not mean that milk industry is not a business. 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)
Food is important for national security so we should subsidize it, but it's a cost center. It'll never drive growth.
If that's what Mistral is aiming for, it would probably be better to give up now.
Earlier quoted context omitted.
well all commodities are like this. replace AI with milk, or plastic. It's easy for me to just move to different milk provider, this does not mean that milk industry is not a business. 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)
It does mean that the milk industry is a low value add commodity business where suppliers compete primarily on price and only survive due to protectionism and subsidies. Food is important for national security so we should subsidize it, but it's a cost center. It'll never drive growth. If that's what Mistral is aiming for, it would probably be better to give up now.
Earlier quoted context omitted.
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 like this format: "I love Lean because . I found it failed in case because . I created a thing which handles that like this: . I'd love feedback! It's open source here: "
Try out Leanstral 1.5 on the latest version of OpenATP! OpenATP is an open-source Python package and CLI for agentic automated theorem provers. It natively supports running provers locally in Docker or remotely in Modal sandboxes. GitHub: https://github.com/henryrobbins/open-atp Docs: https://open-atp.henryrobbins.com
[flagged]
Earlier quoted context omitted.
well all commodities are like this. replace AI with milk, or plastic. It's easy for me to just move to different milk provider, this does not mean that milk industry is not a business. 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)
It does mean that the milk industry is a low value add commodity business where suppliers compete primarily on price and only survive due to protectionism and subsidies. Food is important for national security so we should subsidize it, but it's a cost center. It'll never drive growth. If that's what Mistral is aiming for, it would probably be better to give up now.
There are a whole lot of commodity businesses that flourishes and that are profitable. It's true, that, yes, they will not have huge margins.
Grocery stores are like that - some of their suppliers might be subsidised but they are not, and many places they operate with typical margins in the 2% range. Discount supermarkets in the UK are operating on around 0.7% margins.
They are still huge, profitable businesses.
And they are examples of what happens when markets work.
Earlier quoted context omitted.
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…
well all commodities are like this. replace AI with milk, or plastic. It's easy for me to just move to different milk provider, this does not mean that milk industry is not a business. 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)
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've gone from zero knowledge of lean4 to the point where I'm doing most of my coding with it in ~6 months, and this was dramatically helped by how facile the AI assist is: it's remarkable how consistently fluent models are in lean4. I've found this to be true of the near frontier and smaller local models alike, LLMs just seem to get lean4. I still have a ways to go before calling myself a lean4 expert, but I don't n…