News for hackers. Stuff that matters.

A comment on OpenAI withdraws three mathematical results. Parent comment

Re:OpenAI withdraws three mathematical results by rich_sasha on Thursday October 08, 2026 @04:58AM (#50003467)
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..?

[ Parent | on HN ]
Re:OpenAI withdraws three mathematical results by mcphage on Thursday October 08, 2026 @08:01AM (#50004796)
> 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.

[ Parent | on HN ]
Re:OpenAI withdraws three mathematical results by stavros on Thursday October 08, 2026 @04:59AM (#50003471)
If you're fuzzing the solver, you might discover a solver bug.
[ Parent | on HN ]
Re:OpenAI withdraws three mathematical results by CrimsonRain on Thursday October 08, 2026 @05:45AM (#50003774)
Still a great progress
[ Parent | on HN ]