We don’t need mathematicians to clear the proof as valid if it is checked by a formal proof system. Mathematicians would only need to check the theorem itself to make sure it describes what it should describe.

I think chess and go are a bad comparison. Their solving does not conclude in some societal use. They are interesting only as problems, but mathematics is interesting as a solution too.

How so? Particularly in intuitionist logic it would seem to me that they are the same thing.