>> If future AI systems will produce genuine proofs, logically correct and intelligible, like those produced by “master” mathematicians, it would still be incor

>> If future AI systems will produce genuine proofs, logically correct and intelligible, like those produced by “master” mathematicians, it would still be incorrect to think that mathematics would have been “solved” as some say that chess or Go have been solved. Chess and Go have most definitely not been solved. In AI research when we say that a game (and usually we mean a traditional board game) has been "solved", what we mean is that we can correctly predict the outcome of any game instance from any board position provided both players play perfectly [1]. This can mean we have an algorithm that chooses the perfect play for each player in any position or that we have mapped the entire game tree for that game: every move in every game, from start to finish. There are games that have been solved this way: tic-tac-toe; connect four; nim; othello, checkers. But not chess and Go. Rather, what we have for chess and Go are super-human engines, i.e. computer players that no human has ever beaten in the full game. So for example a chess engine like Stockfish can always choose what move to make in order to win against a human player in any board position. However, that is still not the same as knowing how to play perfectly in any board position. Like the old joke with the two guys trying to outrun a bear, a chess engine doesn't have to play perfect chess to be super-human: it just has to play better than any human. To the extent that chess and Go are games it could be said that winning is the whole point of AI game-playing [2]. But the article above suggests that there is no point of "winning" in maths. In AI chess it is unfortunate that the development of super-human chess engines has ended all research in using AI chess to understand the way that human players play chess (which is to say: not by alpha-beta minimax, or Monte Carlo Tree Search, or anything like that) which was the original reason that luminaries of the field such as Shannon, Minsky, McCarthy, Michie, and even Turing himself were interested in the question in the first place. The concern then for mathematics is that AI "winning" at maths will kill mathematics research and replace it with ... as McCarthy would have it "very fast fruit flies" [3]. _______________ [1] https://en.wikipedia.org/wiki/Solved_game https://en.wikipedia.org/wiki/Solved_game [2] Then again see John McCarthy's criticism of that idea written in the wake of DeepBlue vs Kasparov: https://www-formal.stanford.edu/jmc/newborn/newborn.html https://www-formal.stanford.edu/jmc/newborn/newborn.html [3] ibid.