That's a completely different matter than what this thread was about. This thread was about whether mistakes in the 13M lines of Lean code could mean that this proof could be wrong despite Lean saying it's right.