Leanstral: Open-source agent for trustworthy coding and formal proof engineering • Hacker News Board

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

#91

Post by Aerroon » Tue, Mar 17, 2026, 5:01 AM UTC

cyanydeez wrote: post #22

patall wrote: post #18

Earlier quoted context omitted.

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.

The SD ecosystem in large part was grassroots and focused on nsfw. I think current LLM companies would have a hard time getting that to happen due to their safety stuff.

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

#92

Post by Aerroon » Tue, Mar 17, 2026, 5:10 AM UTC

androiddrew wrote: post #45

re-thc wrote: post #12

Earlier quoted context omitted.

Mistral Small 4 is already announced.

MOE but 120B range. Man I wish it was an 80B. I have 2 GPUs with 62Gib of usable VRAM. A 4bit 80B gives me some context window, but 120B puts me into system RAM

Either some q3 or since it's a MoE, maybe a REAP version of q4 might work (or could be terrible, I'm not sure about REAP'd models).

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

#93

Post by radlad » Tue, Mar 17, 2026, 5:29 AM UTC

stingraycharles wrote: post #80

MillionOClock wrote: post #72

Earlier quoted context omitted.

It is definitely not foolproof but IMHO, to some extent, it is easier to describe what you expect to see than to implement it so I don't find it unreasonable to think it might provide some advantages in terms of correctness.

That definitely depends upon the situation. More often than not, properly testing a component takes me more time than writing it.

In my experience, this tends to be more related to instrumentation / architecture than a lack of ability to describe correct results. TDD is often suggested as a solution.

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

#94

Post by openclaw01 » Tue, Mar 17, 2026, 5:44 AM UTC

[dead]

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

#95

Post by louiskottmann » Tue, Mar 17, 2026, 5:56 AM UTC

rvz wrote: post #86

jatins wrote: post #60

Earlier quoted context omitted.

If Agent is writing the tests itself, does it offer better correctness guarantees than letting it write code and tests?

Given the issues with AWS with Kiro and Github, We already have just a few high-profile examples of what happens when AI is used at scale and even when you let it generate tests which is something you should absolutely not do. Otherwise in some cases, you get this issue [0]. [0] https://sketch.dev/blog/our-first-outage-from-llm-written-co...

The linked article does not speak of tests, it speaks of a team that failed to properly review an LLM refactor then proceeds to blame the tooling.

LLMs are good at writing tests in my experience.

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

#96

Post by westurner » Tue, Mar 17, 2026, 6:06 AM UTC

From https://mistral.ai/news/leanstral :

  Model        Cost ($) Score
  ..
  Claude Opus     1,650 39.6
  ..
  Leanstral pass@8  145 31.0
  Leanstral pass@16 290 31.9

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

#97

Post by trenchgun » Tue, Mar 17, 2026, 6:08 AM UTC

Paracompact wrote: post #76

refulgentis wrote: post #70

Earlier quoted context omitted.

I've seen this sentiment and am a big fan of it, but I was confused by the blog post, and based on your comment you might be able to help: how does Lean help me? FWIW, context is: code Dart/Flutter day to day. I can think of some strawmen: for example, prove a state machine in Lean, then port the proven version to Dart? But I'm not familiar enough with Lean to know if that's like saying "prove moon made of cheese wit…

I don't think he's referring to Lean specifically, but any sort of executable testing methodology. It removes the human in the loop in the confidence assurance story, or at least greatly reduces their labor. You cannot ever get such assurance just by saying, "Well this model seems really smart to me!" At best, you would wind up with AI-Jim. (One way Lean or Rocq could help you directly, though, would be if you coded…

>Such is very difficult at the moment

What do you mean? It's a nice and simple language. Way easier to get started than OCaml or Haskell for example. And LLMs write programs in Lean4 with ease as well. Only issue is that there are not as many libraries (for software, for math proofs there is plenty).

But for example I worked with Claude Code and implemented a shell + most of unix coreutils in like a couple of hours. Claude did some simple proofs as well, but that part is obvs harder. But when the program is already in Lean4, you can start moving up the verification ladder up piece by piece.

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

#98

Post by nicman23 » Tue, Mar 17, 2026, 6:11 AM UTC

rothific wrote: post #46

There have been a lot of conversations recently about how model alignment is relative and diversity of alignment is important - see the recent podcast episode between Jack Clark (co-founder of Anthropic) and Ezra Klein. Many comments here point out that Mistral's models are not keeping up with other frontier models - this has been my personal experience as well. However, we need more diversity of model alignment tech…

they ll get there

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

#99

Post by hrmtst93837 » Tue, Mar 17, 2026, 6:40 AM UTC

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.

[flagged]

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

#100

Post by oakpond » Tue, Mar 17, 2026, 6:44 AM UTC

nextos wrote: post #82

tonymet wrote: post #74

Earlier quoted context omitted.

AI is the reality that TDD never before had the opportunity to live up to

Not just TDD. Amazon, for instance, is heading towards something between TDD and lightweight formal methods. They are embracing property-based specifications and testing à la Haskell's QuickCheck: https://kiro.dev Then, already in formal methods territory, refinement types (e.g. Dafny, Liquid Haskell) are great and less complex than dependent types (e.g. Lean, Agda).

It makes sense to me as long as you're not vibe coding the PBTs.