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 11 hours ago | parent | next [-]

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

	▲	CrimsonRain 10 hours ago \| parent [-]
		Still a great progress

mcphage 8 hours ago | parent | prev [-]

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