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