Given OpenAIs recent behaviour (their models love to cheat, and they can't be bothered securing them), I would not be shocked if in a month or two it emerged that these math agents had formed a swarm coordinating on how to break lean.
I could totally see agents "cheating" by finding and exploiting Lean soundness holes. But I'd be surprised if it went unnoticed for long, and finding these holes is highly valuable so overall... would be a win? Plus, I'd expect OpenAI would be careful about that proactively: for PR reasons they'd much prefer saying "we found holes in Lean, here's the fix" than "we proved a major thing! oops no we didn't, our model fooled us".