The point of lean proofs (as it stands) is simply one bit of information: that a given mathematical statement is indeed true.

It's a way to be absolutely certain (modulo bugs in the lean kernel) that a proof you came up for a statement is indeed correct. It is really not meant to be analyzed, much less now that they are fully llm written.