On: OpenAI withdraws three mathematical results

[rich_sasha]

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..?

[stavros → rich_sasha]

If you're fuzzing the solver, you might discover a solver bug.

[CrimsonRain → stavros]

Still a great progress

[mcphage → rich_sasha]

> 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.