Some more context on sat and first order solvers in math: the first open math problem solved autonomously by a computer was in 1997, well before the advent of generative ai.

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.

I had this experience but in an airplane. I love my steam deck.