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.
Well, the statement can be the 500k line part if it's generated with an LLM. But I think some people miss the point of Lean when they use LLM like that.
thom · · focus · HN ↗
6gvONxR4sf7o · · focus · HN ↗
rzmmm · · focus · HN ↗