>And I don't think that paper addresses it, but if the LLM can find a bug in Lean and exploit it to prove something, there's a good chance it will find it and not report it.

Why would it know it found a bug?

I guess it would result in the same outcome if it knew it exploited a bug (and didn’t disclose that) or not.