Comment by rich_sasha
9 hours ago
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”.
You might think this is not very useful, maybe - but that’s not a reason to retract..?
If you're fuzzing the solver, you might discover a solver bug.
Still a great progress
> 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.