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.
You might think this is not very useful, maybe - but that’s not a reason to retract..?
It may be correct, but it might not be a proof of what OpenAI claims it to be a proof of.