Another danger is some sort of bug in Lean itself. This isn't unprecedented in theorem provers [1][2]. These might be hard to hit by accident... but there are larger and larger collaborations where arbitrarily people fill in steps (like [3]). Someone trolling one of these efforts by filling a step in using a bug they found might become worth worrying about.

[1]: https://inutile.club/estatis/falso/

[2]: https://www.youtube.com/watch?v=sv97pXplxf0

[3]: https://terrytao.wordpress.com/2023/11/18/formalizing-the-pr...