> The problem is, how trustworthy are proof checkers? Are there bugs? And is the underlying theory itself free of paradoxes and unknowables and mathematical "bugs" that can be exploited? Imagine a human mathematician hell bent on deceiving other mathematicians - would we trust their breakthroughs, even with a verifier?

---

> Autumn of verified Lean kernels

Have you read this section (and immediately following sections) in the article? It seems that it partly addresses your thoughts. Perhaps you should comment replying to it.