For normal honest proofs (i.e. not maliciously crafted for exploit) that is almost impossible. The Lean kernel is quite small (de Bruijn Criterion) and trusted. See Probability and the de Bruijn Criterion - https://proofassistants.stackexchange.com/questions/247/prob.... Parts of the kernel have also been independently re-implemented in other languages and compared to ensure that they all yield the same logical result.

Finally, you can export your proofs from Lean and have them re-verified by other independently developed theorem provers/proof checkers.

To get an idea of what is involved in a Theorem Prover see;

Introduction to Automated Theorem Provers - https://pqnelson.github.io/2020/03/27/automated-theorem-prov...

Towards a simple theorem prover - https://medium.com/@maiavictor/towards-a-simple-theorem-prov...