Comment by soVeryTired

Or maybe the PhD impersonator discovered a soundness bug in a component of Lean and was able to exploit it.

With no humans able to understand the proofs the impersonator has produced, there's no way of knowing.