>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.
None of the soundness bugs found in lean so far could have been plausibly exploited by accident. For example you might have to set up weird recursive types that never come up in ordinary mathematics. Of course, past performance is not indicative of future results.
I guess it would result in the same outcome if it knew it exploited a bug (and didn’t disclose that) or not.