Comment by xelxebar

I would expect proofs that exploit kernel bugs to look fishy, so someone reading the proof could catch the smell.

That said, I'm sure there's also room for underhanded Lean programming as well, which would be even more interesting.