If you wrote twenty million lines of Lean to verify something, my suspicion is you've been fuzzing the Lean solver rather than coming up with new math.

▲

rich_sasha 11 hours ago | parent [-]

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.