Comment by minkowski

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.)