I apologize in advance if the question is too naive or not suitable for this website.

There are many artificial intelligence programs whose performance in chess exceeds the best humans at chess (Alphazero comes to mind). As far as I know, there is no such thing as in the domain of mathematics. Why is this the case ? ie what distinguishes the domain of chess from the domain of mathematics from a computational point of view ? After all, mathematics (from a formalist point of view) is very similar to chess as a game in the sense that you start from axioms (similar to the inital position jn a chess game) and manipulate them using the rules of inference of first order logic (similar to rules of chess on how to move pieces)

  • $\begingroup$ First thing that comes to mind for me is that, compared to chess, math is more varied and complex. Current AI is most powerful in domains that are very narrow, where there is already a large corpus of training data (of accurate classification or expert-level "play"). Maybe if Google devoted comparable resources to training an AI on some specific narrow, well-chosen mathematical problem, they might be able to make progress comparable to a human being on that specific problem. But maybe not, e.g. what would they use for training data? $\endgroup$ – Neal Young Jun 10 at 14:04
  • $\begingroup$ @NealYoung training data could be obtained from the library of formalized mathematics of the mizar project for example ?en.m.wikipedia.org/wiki/Mizar_system $\endgroup$ – Amr Jun 10 at 14:32
  • $\begingroup$ Nice. [Somewhat off topic but it would nice to have an AI that could aid a human in building such a proof, by finding proofs of the "smaller" steps.] $\endgroup$ – Neal Young Jun 10 at 17:46
  • $\begingroup$ I'm wondering what an equivalent question could be if asked in the next century :-) $\endgroup$ – Marzio De Biasi Jun 10 at 18:14
  • $\begingroup$ From a formalist point of view, mathematics is actually very far from chess: chess is algorithmically decidable, whereas mathematics is undecidable. $\endgroup$ – Emil Jeřábek Jun 11 at 8:34

Browse other questions tagged or ask your own question.