alt Hacker NewsWell, fine - but my understanding is, if a fuzz-generated Lean proof is correct, that’s end of story. It can’t be “incorrect” if it “passes”.
You might think this is not very useful, maybe - but that’s not a reason to retract..?
Replies
mcphage • today at 12:01 PM
> Well, fine - but my understanding is, if a fuzz-generated Lean proof is correct, that’s end of story. It can’t be “incorrect” if it “passes”.
It may be correct, but it might not be a proof of what OpenAI claims it to be a proof of.
If you're fuzzing the solver, you might discover a solver bug.