alt Hacker News>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?
Replies
Danox • today at 10:44 PM
It doesn’t at the end of the day.
I guess it would result in the same outcome if it knew it exploited a bug (and didn’t disclose that) or not.