Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Leanstral 1.5: Proof abundance for all

mistral.ai

Post reply on HN
Print view View original

81–90 of 116 posts

Re: Leanstral 1.5: Proof abundance for all

#81

Post by InsideOutSanta »

kaashif wrote: post #74
vincnetas wrote: post #65

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.

> If that's what Mistral is aiming for, it would probably be better to give up now.

If Mistral is aiming not to grow to infinity but instead to offer niche models at reasonable prices, should they give up now? I think I'm not sure what exactly you're saying.

Re: Leanstral 1.5: Proof abundance for all

#82

Post by guiriduro »

lou1306 wrote: post #61
nok22kon wrote: post #60

Earlier quoted context omitted.

big AI labs make so much money because they have a good (amazing) product

Do they even _make_ actual money? https://isaiprofitable.com/ seems to disagree.

Do they dupe VC into enormous datacentre and capacity build-out investment? Why yes, actual money going to the AI hypester pick-axe vendors (and early equity dumpers) in that sense, absolutely yes it does.

Is Big AI on track to pay that back with profit from any foreseeable and defensible business model? Different question. I sincerely doubt it.

Re: Leanstral 1.5: Proof abundance for all

#83

Post by raverbashing »

lou1306 wrote: post #61
nok22kon wrote: post #60

Earlier quoted context omitted.

big AI labs make so much money because they have a good (amazing) product

Do they even _make_ actual money? https://isaiprofitable.com/ seems to disagree.

I bet Sam, Dario and others have a good salary and an even better stock plan

The good thing about open capital markets is the possibility to invest in the upside. The downside is who gets holding the bag when the money runs out

Re: Leanstral 1.5: Proof abundance for all

#84

Post by teiferer »

Quekid5 wrote: post #35
boulos wrote: post #2

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…

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.

> 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.

I get what you are saying but does this actually apply to a test? If the code under test is in one compilation unit and the test harness in another and they are linked together then the UB optimization issue ends at the API boundary and can't possibly make the test pass ..?

Re: Leanstral 1.5: Proof abundance for all

#85

Post by barrenko »

numeri wrote: post #80
reinitctxoffset wrote: post #64

Earlier quoted context omitted.

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…

Are you writing general use programs in it, then? Have any good examples?

+1, what is it that you are doing.

Re: Leanstral 1.5: Proof abundance for all

#86

Post by vrganj »

zuzululu wrote: post #29

I 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

As somebody who moved to the US and then back to Europe again, you may get more money there, but you'll pay for it with a much worse environment and lifestyle.

Life's not all about the number on your bank account. Once you're past a certain level (which a competent engineer can easily reach in Europe as well), the marginal utility of money diminished quite quickly.

Re: Leanstral 1.5: Proof abundance for all

#87

Post by ChrisArchitect »

rtaylorgarlock wrote: post #31
ChrisArchitect wrote: post #22

[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.

oh of course, unfortunately people's self-interest in pushing their own submissions and not being told they missed a story causes adverse reactions, but a bit of sacrifice worth keeping the site fresh and discussions focused.

Re: Leanstral 1.5: Proof abundance for all

#88

Post by therealpygon »

vincnetas wrote: post #75
kaashif wrote: post #74

Earlier quoted context omitted.

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.

In some sense all commodities are "important for national security". Generic drugs are important for national security. Computer technology is important for national security. Im not sure what we arguing about. Im saying that AI is good thing to have like other commodity and it should net be one provider worth gazillion money.

Oil and gas is the type of commodity I’d rather it be modeled on, if I had to choose. Something with a lot of competition but an understanding that negative actions can easily affect your bottom line regardless of whether you were the one who took them, so generally better to operate with cooperative competition on the whole.

Re: Leanstral 1.5: Proof abundance for all

#90

Post by andai »

dannyw wrote: post #36
andai wrote: post #14

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.

It’s a 6bn model. Totally different class. I’m more excited about “frontier small language models” tbh.

It's a 119B model, 6B active.

That's still 3-10x smaller than the other models in that graph though (400B, 1T, 1.5T).

Post reply on HN