Yes, for all we know they're exploiting a bug in Lean.

Sadly, if it were a bug the AI would have used it to prove everything, like in the human written hoax of the Collatz conjeture.

Even if a person manually wrote a paper and 10 person manalluy reviewed it, it is possible that all 11 of them made a mistake.