junk theorems aren't the concern, soundness issues in the lean kernel are the concern.

Notably, junk theorems are true. Nobody would debate that the junk theorem is true. The main thing people would say is that junk theorems, while being true, are sensitive to precisely how you encoded mathematics, so despite being true, they are perhaps not conceptually meaningful.

As an example of a junk theorem, sasy you use the definition of the natural numbers using von neumann ordinals

https://en.wikipedia.org/wiki/Set-theoretic_definition_of_na...

Then for any natural numbers n, m, they're implicitly sets. So n \intersect m = min(n,m). This is the wrong way to think about natural numbers. You should not use this ever in proofs. But this isn't because your proofs would be false, but instead because it is a fundamentally confusing way to think about the natural numbers. It is in this sense it is a "junk theorem".