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

Leanstral: Open-source agent for trustworthy coding and formal proof engineering

mistral.ai

Post reply on HN
Print view View original

21–30 of 234 posts

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#21

Post by sa-code »

chucky_z wrote: post #19
lefrenchy wrote: post #6

Does Mistral come close to Opus 4.6 with any of their models?

I use mistral-medium-3.1 for a lot of random daily tasks, along with the vibe cli. I'd state from my personal opinion that mistral is my preferred 'model vendor' by far at this point. They're extremely consistent between releases while each of them just feels better. I also have a strong personal preference to the output. I actively use gemini-3.1-pro-preview, claude-4.6-opus-high, and gpt-5.3-codex as well. I prefer…

Why not Large 3? It's larger and cheaper

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#22

Post by cyanydeez »

patall wrote: post #18
andai wrote: post #13

Earlier quoted context omitted.

This is called a "LLM alloy", you can even do it in agentic, where you simply swap the model on each llm invocation. It does actually significantly boost performance. There was an article on here about it recently, I'll see if I can find it. Edit: https://news.ycombinator.com/item?id=44630724 They found the more different the models were (the less overlap in correctly solved problems), the more it boosted the score.

That sounds quite interesting. Makes me wonder if sooner or later they will have to train multiple independent models that cover those different niches. But maybe we will see that sooner or later. Thanks for the link.

One would think that LoRAs being so successful in StableDiffusion, that more people would be focused on constructing framework based LoRas; but the economics of all this probably preclude trying to go niche in any direction and just keep building the do-all models.

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#23

Post by lsb »

The real world success they report reminds me of Simon Willison’s Red Green TDD: https://simonwillison.net/guides/agentic-engineering-pattern...

> Instead of taking a stab in the dark, Leanstral rolled up its sleeves. It successfully built test code to recreate the failing environment and diagnosed the underlying issue with definitional equality. The model correctly identified that because def creates a rigid definition requiring explicit unfolding, it was actively blocking the rw tactic from seeing the underlying structure it needed to match.

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#26

Post by beernet »

jasonjmcghee wrote: post #8

Curious if anyone else had the same reaction as me This model is specifically trained on this task and significantly[1] underperforms opus. Opus costs about 6x more. Which seems... totally worth it based on the task at hand. [1]: based on the total spread of tested models

Agreed. The idea is nice and honorable. At the same time, if AI has been proving one thing, it's that quality usually reigns over control and trust (except for some sensitive sectors and applications). Of course it's less capital-intense, so makes sense for a comparably little EU startup to focus on that niche. Likely won't spin the top line needle much, though, for the reasons stated.

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#29

Post by miohtama »

beernet wrote: post #26
jasonjmcghee wrote: post #8

Curious if anyone else had the same reaction as me This model is specifically trained on this task and significantly[1] underperforms opus. Opus costs about 6x more. Which seems... totally worth it based on the task at hand. [1]: based on the total spread of tested models

Agreed. The idea is nice and honorable. At the same time, if AI has been proving one thing, it's that quality usually reigns over control and trust (except for some sensitive sectors and applications). Of course it's less capital-intense, so makes sense for a comparably little EU startup to focus on that niche. Likely won't spin the top line needle much, though, for the reasons stated.

Alignment tax directly eats to model quality, double digit percents.
Post reply on HN