I’m my opinion the best days of YouTube were before monetization was a thing. There were plenty of creators back then, and it was a lot less corporate than it is now.

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.