## MathZero, The Classification Problem, and Set-Theoretic Type Theory

David McAllester

Toyota Technological Institute at Chicago

May 14, 2020

AlphaZero learns to play go, chess and shogi at a superhuman level through self play given only the rules of the game. This raises the question of whether a similar thing could be done for mathematics --- a MathZero. MathZero would require a formal foundation and an objective. We propose the foundation of set-theoretic dependent type theory and an objective defined in terms of the classification problem --- the problem of classifying concept instances up to isomorphism. Isomorphism is central to the structure of mathematics.