MathZero，分类问题和集合论类型论
MathZero, The Classification Problem, and Set-Theoretic Type Theory
摘要：
AlphaZero通过只给游戏规则的自我游戏，以超人的水平学习下围棋、国际象棋和将棋。这就提出了一个问题，是否可以为数学做类似的事情-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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
