Post

Turns out 3 of the papers have been retracted based on a sign error in one of them. github.com/openai/math/...

lmao this commit message to describe 3 retractions

omg

So..what I was worrying about was the gap between human formulation of the problem and Lean formulation (I also think Lean verification is a software process so can have bugs but that's another story), but I don't see how you can have a sign error in something that is Lean verified.

I think this was one of the proofs not yet lean verified. (Re lean software bugs: I wish we could all stop talking about that. Yes compilers have bugs and yes Lean did have an unsoundness issue at some point, but when there is a verified lean proof, I wouldn't bet on the lean compiler being wrong.)

Also there is a second independent verifier I believe. Not sure it was used here, but that should make any doubts go away.

I didn't know we all talked about lean bugs? anyway fair enough

Yes I agree with that

Spoke too soon... It seems there are plenty of lean formalizations that don't match the English theorem and are trivially true. I had assumed some basic due-diligence on their part... bsky.app/profile/adol...