Live data from Hacker News

Leanstral 1.5: Proof abundance for all

mistral.ai

51–60 of 116 posts

Re: Leanstral 1.5: Proof abundance for all

#51

Earlier 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!

Self promotion is fine here typically, I’d say the main thing here is it sounds like a tv ad. Try X! And not in response to a question or stated problem.

Here’s a tip, imagine how you’d comment if this wasn’t your library but just one that you knew and used. Would you have commented at all? Would you explain why you’d use it, how, the direct and clear relevance to the article?

Take that and add in that it’s your library.

If you wouldn’t comment otherwise, you’re just advertising a thing where people are. If you would, you’re contributing to a conversation with something you built.

Oh and there’s lots of open source products that have most useful features paid saas or licensed, or it’s an oss library that only talks to a paid saas thing.

Edit - the other thing you can do is just call out the comment at the start as self promotion or a plug, I think your work is more directly relevant here and doesn’t need that but it’s another approach when it’s a bit more tangential. That’s better here than other communities.

Re: Leanstral 1.5: Proof abundance for all

#52

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…

Stupid Europoors, optimizing for making a good product, instead of optimizing for making as much money as possible /s

Re: Leanstral 1.5: Proof abundance for all

#53

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 would argue it is more valuable

Re: Leanstral 1.5: Proof abundance for all

#54

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?

You need to understand the bits you are trying to prove, but not the full proof. It's more like reading haskell types than math, even though the vocabulary is heavily inspired by math.

Re: Leanstral 1.5: Proof abundance for all

#55

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.

I think there is a non-zero chance that Europe stumbled into an optimal scenario where they avoided all the losses incurred by US companies, but still benefit from the research. Having said that, doing so would require moving at the exact right time.

I wouldn't underestimate the capability of European companies to build rock-solid industries on established science. We may not be the pioneers wedging new product categories into the market, but there are millions of highly qualified people here, working hard every day.

For example, Mercedes autonomous driving team is moving ahead at glacial speed, but the system they have so far is excellent and reliable. I'd prefer that over the sad joke Tesla is promoting any day.

Re: Leanstral 1.5: Proof abundance for all

#56

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.

Re: Leanstral 1.5: Proof abundance for all

#57

Earlier 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!

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: "

Re: Leanstral 1.5: Proof abundance for all

#58
post #56

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.

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.

Re: Leanstral 1.5: Proof abundance for all

#59
post #56

Earlier quoted context omitted.

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.

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

Re: Leanstral 1.5: Proof abundance for all

#60

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…

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
Post reply on HN