Fetching the paper…

Reading the bibliography…

2020

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

McAllester, David

Original
PDF
Post on X

Understand

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.

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

Built on

Lattice Theory, 3rd edition
Birkhoff, G · 1967
Earlier work this paper cites.
On the foundations of combinatorial theory: Combinatorial geometries
Crapo, H. and Rota, G.-C · 1970
Earlier work this paper cites.

Similar

An intuitionistic theory of types: predicative part
Per Martin Löf · 1975
Cited alongside, same era.
The coq proof assistant reference manual: Version 6.1
B. Barras, S. Boutin, C. Cornes, J. Courant, J.C. Filliatre, E. Gimenez, H. Herbelin, G. Huet, C. Munoz, C. Murthy, et al · 1997
Cited alongside, same era.

Then

The groupoid interpretation of type theory
Martin Hofmann and Thomas Streicher · 1998
Later among the works it cites.

Beyond the bibliography

alphaXiv searches the wider corpus for related work and actual follow-ups.

Open on alphaXiv

alphaXiv is searching for related work…