Unless humans understand them, can we trust such formalisations? We can prove the formalisation is correct, but we can't prove it accurately reflects what we are trying to prove.
Of course, one has to convince oneself the Lean theorem is defined correctly, but it will be orders of magnitude shorter than the proof. (In this case, one would also need to assume that probability theory, random graphs, etc. are defined correctly, but one would generally be happy to leave this to others.)