But that's where you're wrong. All 12 million lines do not need to be checked (again, that's literally the entire purpose of Lean). All that needs to be checked is that the proposition of the theorem is what we think it is, and that has been done. What Lean guarantees is that if you start with a set of axioms -> whole bunch of steps that nobody really ever needs to read -> final theorem proposition, that those steps do successfully prove the theorem.
You say "it's not hard to have a Lean statement that isn't what you think it is", and that's true - indeed, what the entire paper is about is that the intermediate steps in Lean don't match the natural language description. But the statement of the proof in Lean (which again is quite short) is what we think it is, and hence the Lean proof is valid.
You say "it's not hard to have a Lean statement that isn't what you think it is", and that's true - indeed, what the entire paper is about is that the intermediate steps in Lean don't match the natural language description. But the statement of the proof in Lean (which again is quite short) is what we think it is, and hence the Lean proof is valid.