alt Hacker NewsCan 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?