论文标题
Mathzero，分类问题和设定理论理论
MathZero, The Classification Problem, and Set-Theoretic Type Theory
论文作者
论文摘要
Alphazero学会了通过自我玩法在超人级别上打球，国际象棋和Shogi，只有游戏规则。这就提出了一个问题，即是否可以为数学做类似的事情-MathZero。 Mathzero将需要正式的基础和目标。我们提出了集合理论依赖类型理论的基础，以及根据分类问题定义的目标 - 将概念实例分类为同构的问题。自然数是作为有限集的分类问题解决方案的。在这里，我们将经典的布尔巴基集体理论同构概括为设定依赖类型的理论。据我们所知，我们给出了与命题设定理论平等的第一个相关类型理论的同构推理规则。该演讲旨在访问数学家，而没有事先接触类型理论。
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.
