Comment by stavros
8 hours ago
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.
8 hours ago
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.
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.