This is a crucial point. There have been many bugs in Lean (and in other proof assistants for that matter). Proof assistants work well on human input, because it was created with a certain intent.

We simply don’t know what those 13M contain and whether it “makes sense” and doesn’t trigger Lean bugs. (There are “independent” lean verifiers, but historically they contained the same, or similar, bugs.)