> Do you also have to review the proof checking code to make sure you didn't make any errors in transcription from the original paper?

The point of the checked proof is that your final theorem is almost definitely correct (you did not make mistakes in your deductions, unless the proof checker has a serious bug) if you can convince computer it derives from your axioms.

You can convince humans without your proof being correct thought, because they might not spot an error.

There is a language called lean which is popular among mathematicians. Here is an article: https://www.quantamagazine.org/building-the-mathematical-lib...

A more recent article as well: https://www.quantamagazine.org/lean-computer-program-confirm...

My question was specifically referring to these huge 500 proofs that only a handful of people have even attempted to understand. What is the upper limit of what our current state-of-the-art proof assistants can handle?

The problem is not the limit of what proof checkers can handle - that probably goes beyond all known math. The problem is that long standing theories that 500 page proof is based on are not yet transcribed into formal language, so you'd need to do them first.