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.
This. Lean does not remove human responsibility, but it does assist in reducing the surface that the human needs to inspect and verify.
Now, there is also debate about what is lost when humans don't understand the proof body itself. It's a fair concern, and one we'll probably be wrestling with for some years.
thom · · focus · HN ↗
6gvONxR4sf7o · · focus · HN ↗
ubj · · focus · HN ↗
Now, there is also debate about what is lost when humans don't understand the proof body itself. It's a fair concern, and one we'll probably be wrestling with for some years.