He could not freely disclose and publish his results, that was the whole problem. He only got traction when one result was automatically validated because Hardy had already seen it. His findings more broadly were only considered fine once they were understood and verified. This declaration is basically the same thing. Having Lean code doesn't substantially change that.

It's almost like a lot of non-mathematicians are commenting and have no idea about how the field really works. Or at least, how it works at the top level.