MathZero, The Classification Problem, and Set-Theoretic Type Theory
This work addresses foundational challenges in automating mathematical reasoning, though it appears incremental as it builds on existing type theory and classification concepts.
The paper tackles the problem of formalizing a MathZero system for mathematics by proposing set-theoretic dependent type theory as a foundation and the classification problem as an objective, resulting in the first isomorphism inference rules for this theory with propositional set-theoretic equality.
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. The natural numbers arise as the solution to the classification problem for finite sets. Here we generalize classical Bourbaki set-theoretic isomorphism to set-theoretic dependent type theory. To our knowledge we give 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.