[pvillano]

You don't need to check the proof. A regular proof is written to convince other mathematicians. A regular proof can skip details and contain mistakes. A formal proof cannot skip details or contain mistakes.

A lean proof is a sequence of instructions that starts with a list of facts, and combines them into new facts until a target fact is produced. Each instruction in the sequence is one of a few allowed tactics provided by lean that always produce correct facts from correct facts.

IF (1) you agree with the starting facts, (2) you are sure the target fact is what you're actually trying to prove and (3) the lean compiler says "yep, this is a valid sequence of instructions" THEN you can be sure the target fact is true.

You can be sure the final fact is true, even if you don't understand all the steps, because it's written in lean, and lean only allows steps that are free from omissions or errors