Current trendy AI technologies are great for producing solutions but not good at confirming they're good solutions. So, there's increasing need for ways to confirm the solutions. Theorem proving is a way to do this.
Some of the end goals could be: (1) program verification becomes something that's done by default, (2) the entire mathematics literature becomes formalized and verified (and all errors there found and corrected), with programs able to read and formalize papers from the old literature, and (3) new mathematics is done largely by computer, with people acting as "is this interesting?" filters more than agents of discovery. I don't see any reason why mathematics should be immune to domination by computers, any more than (say) Go (the game) was.
pfdietz|1 year ago
Some of the end goals could be: (1) program verification becomes something that's done by default, (2) the entire mathematics literature becomes formalized and verified (and all errors there found and corrected), with programs able to read and formalize papers from the old literature, and (3) new mathematics is done largely by computer, with people acting as "is this interesting?" filters more than agents of discovery. I don't see any reason why mathematics should be immune to domination by computers, any more than (say) Go (the game) was.