There is a simple piece of code that can check simple steps, and many people agree this checker is correct. Then there is a formalization of the theorem which many people agree defines the theorem accurately. Then there is 13 million lines of proof that nobody has read, but the proof checker validated each step. That's enough.

So, all you have to verify is the formalization of the theorem, and believe that the proof checker is free of bugs. You don't have to read the actual proof.

This was my question as well. The way I understand it, it's like a compiler, it implements rules, in this case logic/math rules that tell you whether something follows from assumptions you've given it.

But how do you know you told it what you intended to tell it?

A human definitely didn't, but one of the benefits of formal verification is that even if the work done to achieve something is slop-y or excessively verbose, solvers like Lean guarantee that the initial proposition (assuming it was written correctly and in this case was definitely reviewed by humans) is definitively True. This is true across other domains of formal verification outside of math as well

The point of writing Lean code is that Lean checks it accordingly. Lean is a domain specific language to encode mathematical reasoning in a way that can’t be fooled.

Note to other users: don’t downvote this kind of comment, answer it.

The nice thing about theorem provers is that you don't need to read the intermediate lines. You need to make sure that the goal/result actually matches what you think it says - but everything in the middle is validated by the prover.

No. No human checked it. But a type checker did. And that is much better.