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.)

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).