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

171–180 of 234 posts

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

#171

Post by xpe »

AlotOfReading wrote: post #88
specvsimpl wrote: post #83

Earlier quoted context omitted.

Uhm, no? Even with "simple" examples like Dijkstra's shortest path, the spec is easier than the implementation. Maybe not for you, but try it out on an arbitrary 5-yr old. On the extreme end, you have results in maths, like Fermat's Last Theorem. Every teenager can understand the statement (certainly after 10 mins of explanation) but the proof is thousands of pages of super-specialized maths. It is a spectrum. For cr…

I don't know why you created a new account for this, but take the textbook example of a nontrivial formally verified system: SeL4. That implementation was 8.7k of C code, which correspondend to 15k lines of Isabelle that ultimately needed 100k+ lines of proof to satisfy. And that was with the formal model excluding lots of important properties like hardware failure that actual systems deal with.

> I don't know why you created a new account for this

What value does this add to the conversation? I’m not seeing it: am I missing something? It comes across as a kind of insult.

They made a good point in my opinion! (The “Uhm no” part got it off on the wrong foot, I will admit.) But even if you felt annoyed or didn’t agree with the point, it was substantive and moved the conversation forward. I’m here for the (genuine) questions and (constructive) debate and (civil) pushback.

I like to welcome new users before they take too much of a beating. That can come later when they are too invested to leave and/or when morale needs improving.

So welcome! Bring a helmet, and don’t stop disagreeing.

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

#172

Post by naasking »

hobofan wrote: post #103
speedgoose wrote: post #101

Earlier quoted context omitted.

But you can run this model for free on a common battery powered laptop sitting on your laps without cooking your legs.

Sorry, but what are you talking about? This is a 120B-A6B model, which isn't runnable on any laptop except the most beefed up Macbooks, and then will certainly drain its battery and cook your legs.

You can easily run a quant of this on a DGX Spark though. Seems like a small investment if it meaningful improves Lean productivity.

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

#173

Post by naasking »

TimTheTinker wrote: post #68
drdaeman wrote: post #61

Can someone please explain... If I don't know any Lean (and I suspect most people don't), is it of any direct value? Trying to understand if there's something it can help me with (e.g. automatically write proofs for my Go programs somehow... I'm not sure) or should I just cheer solely for more open models out there, but this one isn't for me?

Presumably the idea is that an agent generates a Lean4 specification against which the software is measured. But then the Lean4 specification effectively becomes the software artifact. And we're sort of back to square 1. How do you verify a Lean4 spec is correct (and that it describes what needs to be built in the first place) without human review?

> And we're sort of back to square 1.

Specifications are smaller than the full code, just as high level code is smaller than the functionally equivalent assembly. As we ascend the abstraction ladder the amount of reading a human needs to do decreases. I don't think this should really count as "back to square 1".

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

#174

Post by xpe »

jasonjmcghee wrote: post #50
JoshTriplett wrote: post #35

Pleasant surprise: someone saying "open source" and actually meaning Open Source . It looks like the weights are Apache-2.0 licensed.

Based on community definitions I've seen, this is considered "open weights". If you can't reproduce the model, it's not "open source"

Yes “open weights” conveys the reality more clearly: merely having the parameters is very different than able to run a process that creates them. Without openness of the full process start to finish, much is hidden.*

Remember, language is what we make it. Dictionaries are useful catalogs of usage but we make the judgment calls.

* Even with the process, much is not well understood! / The ethics of releasing an open weights model at some capability level is a separate discussion.

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

#175

Post by SiempreViernes »

discreteevent wrote: post #158
ptidhomme wrote: post #141

Earlier quoted context omitted.

The theory still emanated from actual observations, didn't it ?

It did but they were meaningless without a human intellect trying to make sense of them.

No, the theory comes from the authors knowledge, culture and inclinations, not from the fact.

Obviously the author has to do much work in selecting the correct bits from this baggage to get a structure that makes useful predictions, that is to say predictions that reproduces observable facts. But ultimately the theory comes from the author, not from the facts, it would be hard to imagine how one can come up with a theory that doesn't fit all the facts known to an author if the theory truly "emanated" from the facts in any sense strict enough to matter.

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

#176

Post by agentultra »

Very cool but I haven’t been able to convince software developers in industry to write property based tests. I sometimes joke that we will start writing formal proofs until the tests improve. Just so that they will appreciate the difference a little more.

I can’t even convince most developers to use model checkers. Far more informal than a full proof in Lean. Still highly useful in many engineering tasks. People prefer boxes and arrows and waving their hands.

Anyway, I don’t know that I’d want to have a system vibe code a proof. These types of proofs, I suspect, aren’t going to be generated to be readable, elegant, and be well understood by people. Like programs they generate it will look plausible.

And besides, you will still need a human to review the proof and make sure it’s specifying the right things. This doesn’t solve that requirement.

Although I have thought that it would be useful to have a system that could prove trivial lemmas in the proof. That would be very neat.

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

#178

Post by rigorclaw »

baq wrote: post #134
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…

yesterday I had to tell a frontier model to translate my code to tla+ to find a tricky cache invalidation bug which nothing could find - gpt 5.4, gemini 3.1, opus 4.6 all failed. translation took maybe 5 mins, the bug was found in seconds, total time to fix from idea to commit - about 15 mins. if you can get a model to quickly translate a relevant subset of your code to lean to find tricky bugs and map lean fixes bac…

[flagged]

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

#179

Post by rowanG077 »

agentultra wrote: post #176

Very cool but I haven’t been able to convince software developers in industry to write property based tests. I sometimes joke that we will start writing formal proofs until the tests improve. Just so that they will appreciate the difference a little more. I can’t even convince most developers to use model checkers. Far more informal than a full proof in Lean. Still highly useful in many engineering tasks. People pref…

The point is you just need to scrutinize the theorem. Not easy either, but still significantly less work than writing the proof.

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

#180

Post by xpe »

esperent wrote: post #39

I absolutely called this a couple of weeks ago, nice to be vindicated! > 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 compile…

[dead]
Post reply on HN