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

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. Mathematics is organized around concepts such as graphs, groups, topological spaces and manifolds each of which is associated with a notion of isomorphism. Each concept is associated with a classification problem --- the problem of enumerating the instances of a given concept up to isomorphism. The natural numbers arise as the solution to the classification problem for finite sets. In this talk we attempt to set the stage for MathZero by giving what we believe to be the first isomorphism inference rules for set-theoretic dependent type theory with propositional set-theoretic equality. The presentation is intended to be accessible to mathematicians with no prior exposure to type theory.