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.

Agreed. There is a much larger likelihood of misformalized statements or wrong interpretation of the formal proof in the write up See: arxiv.org/abs/2610.08144 (also, hi! long time no see, Shreyas from MFoCS).

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

Sorry; I've seen too many threads where people hint at "I don't trust the lean verifier"... I just don't think that's a valid response here.