> Mostly pretty straight forward. The idea that proofs be desloppified, attribute existing literature properly, and published somewhere expediently where it can be commented on, with artifacts for verification, is all very uncontroversial stuff.
If Ramanujan could freely disclose and publish results that were arrived at by literal divine inspiration (he certainly didn't bother to write down "proofs" in the modern sense!) why do we suddenly need all this "responsible release" process stuff when it comes to AI-derived results? This makes no sense when compared with existing norms within the mathematical community.
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.
If Ramanujan could freely disclose and publish results that were arrived at by literal divine inspiration (he certainly didn't bother to write down "proofs" in the modern sense!) why do we suddenly need all this "responsible release" process stuff when it comes to AI-derived results? This makes no sense when compared with existing norms within the mathematical community.