>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.
replyWhy 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.
replyIt doesn’t at the end of the day.
reply