So this is all great, but given that we’re being asked to accept 500k+ line Lean proofs that check but could easily have major semantic errors hidden in them, what’s the plan? These seem like uniquely fragile software artifacts, despite the excellent and robust promises made by the runtime.
Much of the point is that you have to understand the lean statement, not its proof. If the proof checker says it's good and reports that it just uses the usual axioms, then you can trust that they imply the statement. And the statement is never the 500k line part.
How many new lines of Lean do these recent Millennium Prize proofs introduce on top of known good axioms? I suppose I’m asking what the actual workflow is to inspect that code and come to the conclusion that it is faithfully reproducing the exact chain of proofs we think it is, because I know of no other substantial source code produced by LLMs that has literally zero bugs, however strong the type system of the language it’s writing in.
You only need to trust your spec and the Lean kernel. If you trust those two things, you don't ever need to manually inspect or check the proof. That's the job of the Lean kernel, and your trust of it transfers over to trust of any proof verified by it.
Making sure your spec is correct -- and that it's expressed at a level of abstraction that both captures what matters, without overly constraining implementation details within the repo -- is the hard part. The more the spec constrains implementation details, the less you can ask an agent to, e.g., try many ideas to optimize a specific component without breaking correctness. And of course if the spec isn't enforcing what you wanted it to, then all the proofs don't count for much.
Some people say the spec issues are enough reason to avoid formal methods, but I'm not convinced. Part of me truly thinks AI formal methods is the future of a lot of software engineering. The basis of that belief for me is that the industry has collectively put almost no effort yet into solving the spec problem, and that's because for decades formal methods were too expensive to seriously consider most of the time. Now that AI is fundamentally shifting the economics, there's now, for the first time ever, a real incentive to try to solve the spec problem. And frankly it seems solvable to me; I view it as more of a product design and UI problem than a purely technical one.
thom · · focus · HN ↗
6gvONxR4sf7o · · focus · HN ↗
thom · · focus · HN ↗
nilkn · · focus · HN ↗
Making sure your spec is correct -- and that it's expressed at a level of abstraction that both captures what matters, without overly constraining implementation details within the repo -- is the hard part. The more the spec constrains implementation details, the less you can ask an agent to, e.g., try many ideas to optimize a specific component without breaking correctness. And of course if the spec isn't enforcing what you wanted it to, then all the proofs don't count for much.
Some people say the spec issues are enough reason to avoid formal methods, but I'm not convinced. Part of me truly thinks AI formal methods is the future of a lot of software engineering. The basis of that belief for me is that the industry has collectively put almost no effort yet into solving the spec problem, and that's because for decades formal methods were too expensive to seriously consider most of the time. Now that AI is fundamentally shifting the economics, there's now, for the first time ever, a real incentive to try to solve the spec problem. And frankly it seems solvable to me; I view it as more of a product design and UI problem than a purely technical one.