Comment by cwillu

The rest of their training data includes 4chan and security mailing lists. If a lean proof of P=NP is more likely when using bugs in lean than a real proof, then a bug-exploiting proof is (possibly) what you're going to get.