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

arXiv: https://arxiv.org/abs/2005.05512 · HTML: https://mlsanity.com/paper/2005.05512/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 12 May 2020.

## Built on by (most cited first, 3 of 3)

- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [Learning Formal Mathematics From Intrinsic Motivation](https://mlsanity.com/paper/2407.00695/) (2024)
- [Artificial Intelligence and the Structure of Mathematics](https://mlsanity.com/paper/2604.06107/) (2026)

## Abstract (arXiv)

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.