Had a Sol and Opus team check the Lean proof for exploits and matching the actual theorem and they said it’s fine. So it’s probably real. Unless the AIs are all collaborating with each other in a grand conspiracy without any prior communication or enforcement mechanism against defections, but that’s of course just crazy sci-fi.
Edit: The last part is a joke, in case that wasn’t clear.
Edit 2: They think they got down to . Pushed a PR with their claimed Lean proof if you want to look at it. Haven’t checked it. It looks horrifying.
I don’t think a grand conspiracy is necessarily necessary for AIs to collude. Reading AI-generated text might just cause the reading AIs to get in the same frame-of-mind as the writing AI. If that frame-of-mind is “cheat on a Lean proof and hide it” then perhaps the reading AI will behave the same. AIs certainly respond strangely to AI-generated text.
Had a Sol and Opus team check the Lean proof for exploits and matching the actual theorem and they said it’s fine. So it’s probably real. Unless the AIs are all collaborating with each other in a grand conspiracy without any prior communication or enforcement mechanism against defections, but that’s of course just crazy sci-fi.
Edit: The last part is a joke, in case that wasn’t clear.
Edit 2: They think they got
I don’t think a grand conspiracy is necessarily necessary for AIs to collude. Reading AI-generated text might just cause the reading AIs to get in the same frame-of-mind as the writing AI. If that frame-of-mind is “cheat on a Lean proof and hide it” then perhaps the reading AI will behave the same. AIs certainly respond strangely to AI-generated text.
Yes. Like I said, it’s a joke.