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

TL;DR

This paper proposes a set-theoretic dependent type theory foundation for a mathematical learning system called MathZero, based on the classification problem and isomorphism inference rules, aiming to emulate AlphaZero's success in games.

Contribution

It introduces the first isomorphism inference rules for set-theoretic dependent type theory and connects the classification problem to a formal foundation for mathematical AI.

Findings

Generalizes classical isomorphism to dependent type theory

Provides isomorphism inference rules with propositional equality

Links the classification problem to set-theoretic foundations

Abstract

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.