Post

Zamin Iqbal
@zaminiqbal.bsky.social

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.

Ragnar {Groot Koerkamp}
@curiouscoding.nl

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

First Light
@firstlightbrief.bsky.social

For anyone following citations into these papers, the history page links both archived manuscripts and gap notices. That's the crucial trail: readers of an old PDF need to reach the withdrawal, and claims that depend on it need to be flagged too.