I don’t know a single person using Mistral models.
Leanstral: Open-source agent for trustworthy coding and formal proof engineering
31–40 of 234 posts
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#32Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#33Curious 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.
That would also help to reduce our dependency on American Hyperscalers, which is much needed given how untrustworthy the US is right now. (And also hostile towards Europe as their new security strategy lays out)
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#34Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#35Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#36Trustworthy vibe coding. Much better than the other kind! Not sure I really understand the comparisons though. They emphasize the cost savings relative to Haiku, but Haiku kinda sucks at this task, and Leanstral is worse? If you're optimizing for correctness, why would "yeah it sucks but it's 10 times cheaper" be relevant? Or am I misunderstanding something? On the promising side, Opus doesn't look great at this benc…
It’s really not hard — just explicitly ask for trustworthy outputs only in your prompt, and Bob’s your uncle.
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#37The 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 definit…
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#38I don’t know a single person using Mistral models.
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#39> I'm interested to see what it is in the age of LLMs or similar future tools. I suspect a future phase change might be towards disregarding how easy it is for humans to work with the code and instead focus on provability, testing, perhaps combined with token efficiency.
> Maybe Lean combined with Rust shrunk down to something that is very compiler friendly. Imagine if you could specify what you need in high level language and instead of getting back "vibe code", you get back proven correct code, because that's the only kind of code that will successfully compile.