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