“Generative Language Modeling for Automated Theorem Proving § Experiments”, Stanislas Polu, Ilya Sutskever2020 (LM tokenization, GPT, math)