[zozbot234]

You don't have to trust the full Lean toolchain, only the trusted proof kernel (which is small enough to be understood by a human) and any desugarings involved in converting the theorem statement from high-level Lean to whatever the proof kernel accepts (these should also be simple enough). The proof itself can be checked automatically.

[tuhgdetzhh]

Lets assume the kenerl is correct and a mathematian trusts it, now what happens if it is the proof itself that he cannot understand anymore because it has gotten too sophisticated? I think that this would indeed be a difference, and a crossing point in history of mathematical proofs.

[zozbot234]

In principle, it's no different than failing to understand the details of any calculation. If the calculating process is executed correctly, you can still trust the outcome.