Comment by 6gvONxR4sf7o

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.